matrix_7.miz



    begin

    reserve k,n,i,j for Nat;

    theorem :: MATRIX_7:1

    

     Th1: for f be Permutation of ( Seg 2) holds f = <*1, 2*> or f = <*2, 1*>

    proof

      let f be Permutation of ( Seg 2);

      

       A1: ( rng f) = ( Seg 2) by FUNCT_2:def 3;

      2 in {1, 2} by TARSKI:def 2;

      then

       A2: (f . 2) in ( Seg 2) by A1, FINSEQ_1: 2, FUNCT_2: 4;

      

       A3: ( dom f) = ( Seg 2) by FUNCT_2: 52;

      then

      reconsider p = f as FinSequence by FINSEQ_1:def 2;

      

       A4: ( len p) = 2 by A3, FINSEQ_1:def 3;

      

       A5: 1 in ( dom f) & 2 in ( dom f) by A3;

      1 in {1, 2} by TARSKI:def 2;

      then

       A6: (f . 1) in ( Seg 2) by A1, FINSEQ_1: 2, FUNCT_2: 4;

      now

        per cases by A6, A2, FINSEQ_1: 2, TARSKI:def 2;

          case (f . 1) = 1 & (f . 2) = 1;

          hence contradiction by A5, FUNCT_1:def 4;

        end;

          case (f . 1) = 1 & (f . 2) = 2;

          hence thesis by A4, FINSEQ_1: 44;

        end;

          case (f . 1) = 2 & (f . 2) = 1;

          hence thesis by A4, FINSEQ_1: 44;

        end;

          case (f . 1) = 2 & (f . 2) = 2;

          hence contradiction by A5, FUNCT_1:def 4;

        end;

      end;

      hence thesis;

    end;

    theorem :: MATRIX_7:2

    

     Th2: for f be FinSequence st f = <*1, 2*> or f = <*2, 1*> holds f is Permutation of ( Seg 2)

    proof

      let f be FinSequence;

      assume

       A1: f = <*1, 2*> or f = <*2, 1*>;

      ( len <*1, 2*>) = 2 & ( len <*2, 1*>) = 2 by FINSEQ_1: 44;

      then

       A2: ( dom f) = ( Seg 2) by A1, FINSEQ_1:def 3;

      ( rng f) c= ( Seg 2)

      proof

        let y be object;

        assume y in ( rng f);

        then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        then y = (f . 1) or y = (f . 2) by A2, FINSEQ_1: 2, TARSKI:def 2;

        then y = 1 or y = 2 or (y = 2 or y = 1) by A1, FINSEQ_1: 44;

        hence thesis;

      end;

      then

      reconsider g = f as Function of ( Seg 2), ( Seg 2) by A2, FUNCT_2: 2;

      now

        per cases by A1;

          case

           A3: f = <*1, 2*>;

          for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

          proof

            let x1,x2 be object;

            assume that

             A4: x1 in ( dom f) & x2 in ( dom f) and

             A5: (f . x1) = (f . x2);

            now

              per cases by A2, A4, FINSEQ_1: 2, TARSKI:def 2;

                case x1 = 1 & x2 = 1;

                hence thesis;

              end;

                case

                 A6: x1 = 1 & x2 = 2;

                then (f . x1) = 1 by A3, FINSEQ_1: 44;

                hence contradiction by A3, A5, A6, FINSEQ_1: 44;

              end;

                case

                 A7: x1 = 2 & x2 = 1;

                then (f . x1) = 2 by A3, FINSEQ_1: 44;

                hence contradiction by A3, A5, A7, FINSEQ_1: 44;

              end;

                case x1 = 2 & x2 = 2;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

          then

           A8: f is one-to-one by FUNCT_1:def 4;

          now

            let x be object;

            assume x in ( rng f);

            then

            consider z be object such that

             A9: z in ( dom f) and

             A10: (f . z) = x by FUNCT_1:def 3;

            ( len f) = 2 by A3, FINSEQ_1: 44;

            then ( dom f) = ( Seg 2) by FINSEQ_1:def 3;

            then z = 1 or z = 2 by A9, FINSEQ_1: 2, TARSKI:def 2;

            then x = 1 or x = 2 by A3, A10, FINSEQ_1: 44;

            hence x in ( Seg 2);

          end;

          then

           A11: ( rng f) c= ( Seg 2);

          ( Seg 2) c= ( rng f)

          proof

            let z be object;

            assume z in ( Seg 2);

            then z = 1 or z = 2 by FINSEQ_1: 2, TARSKI:def 2;

            then

             A12: z = (f . 1) or z = (f . 2) by A3, FINSEQ_1: 44;

            1 in ( dom f) & 2 in ( dom f) by A2;

            hence thesis by A12, FUNCT_1:def 3;

          end;

          then ( rng f) = ( Seg 2) by A11;

          then g is onto by FUNCT_2:def 3;

          hence thesis by A8;

        end;

          case

           A13: f = <*2, 1*>;

          for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

          proof

            let x1,x2 be object;

            assume that

             A14: x1 in ( dom f) & x2 in ( dom f) and

             A15: (f . x1) = (f . x2);

            now

              per cases by A2, A14, FINSEQ_1: 2, TARSKI:def 2;

                case x1 = 1 & x2 = 1;

                hence thesis;

              end;

                case

                 A16: x1 = 1 & x2 = 2;

                then (f . x1) = 2 by A13, FINSEQ_1: 44;

                hence contradiction by A13, A15, A16, FINSEQ_1: 44;

              end;

                case

                 A17: x1 = 2 & x2 = 1;

                then (f . x1) = 1 by A13, FINSEQ_1: 44;

                hence contradiction by A13, A15, A17, FINSEQ_1: 44;

              end;

                case x1 = 2 & x2 = 2;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

          then

           A18: f is one-to-one by FUNCT_1:def 4;

          now

            let x be object;

            assume x in ( rng f);

            then

            consider z be object such that

             A19: z in ( dom f) and

             A20: (f . z) = x by FUNCT_1:def 3;

            ( len f) = 2 by A13, FINSEQ_1: 44;

            then ( dom f) = ( Seg 2) by FINSEQ_1:def 3;

            then z = 1 or z = 2 by A19, FINSEQ_1: 2, TARSKI:def 2;

            then x = 2 or x = 1 by A13, A20, FINSEQ_1: 44;

            hence x in ( Seg 2);

          end;

          then

           A21: ( rng f) c= ( Seg 2);

          ( Seg 2) c= ( rng f)

          proof

            let z be object;

            assume z in ( Seg 2);

            then z = 1 or z = 2 by FINSEQ_1: 2, TARSKI:def 2;

            then

             A22: z = (f . 2) or z = (f . 1) by A13, FINSEQ_1: 44;

            2 in ( dom f) & 1 in ( dom f) by A2;

            hence thesis by A22, FUNCT_1:def 3;

          end;

          then ( rng f) = ( Seg 2) by A21;

          then g is onto by FUNCT_2:def 3;

          hence thesis by A18;

        end;

      end;

      hence thesis;

    end;

    theorem :: MATRIX_7:3

    

     Th3: ( Permutations 2) = { <*1, 2*>, <*2, 1*>}

    proof

      now

        let x be object;

        assume

         A1: x in {( idseq 2), <*2, 1*>};

        now

          per cases by A1, TARSKI:def 2;

            case x = ( idseq 2);

            hence x in ( Permutations 2) by MATRIX_1:def 12;

          end;

            case

             A2: x = <*2, 1*>;

             <*2, 1*> is Permutation of ( Seg 2) by Th2;

            hence x in ( Permutations 2) by A2, MATRIX_1:def 12;

          end;

        end;

        hence x in ( Permutations 2);

      end;

      then

       A3: {( idseq 2), <*2, 1*>} c= ( Permutations 2);

      now

        let p be object;

        assume p in ( Permutations 2);

        then

        reconsider q = p as Permutation of ( Seg 2) by MATRIX_1:def 12;

        q = <*1, 2*> or q = <*2, 1*> by Th1;

        hence p in {( idseq 2), <*2, 1*>} by FINSEQ_2: 52, TARSKI:def 2;

      end;

      then ( Permutations 2) c= {( idseq 2), <*2, 1*>};

      hence thesis by A3, FINSEQ_2: 52;

    end;

    theorem :: MATRIX_7:4

    

     Th4: for p be Permutation of ( Seg 2) st p is being_transposition holds p = <*2, 1*>

    proof

      let p be Permutation of ( Seg 2);

      assume

       A1: p is being_transposition;

      now

        set p0 = <*1, 2*>;

        assume

         A2: p = <*1, 2*>;

        consider i,j be Nat such that

         A3: i in ( dom p) and

         A4: j in ( dom p) & i <> j and

         A5: (p . i) = j and (p . j) = i and for k be Nat st k <> i & k <> j & k in ( dom p) holds (p . k) = k by A1;

        ( len p0) = 2 by FINSEQ_1: 44;

        then

         A6: ( dom p) = {1, 2} by A2, FINSEQ_1: 2, FINSEQ_1:def 3;

        then

         A7: i = 1 or i = 2 by A3, TARSKI:def 2;

        now

          per cases by A4, A6, A7, TARSKI:def 2;

            case i = 1 & j = 2;

            hence contradiction by A2, A5, FINSEQ_1: 44;

          end;

            case i = 2 & j = 1;

            hence contradiction by A2, A5, FINSEQ_1: 44;

          end;

        end;

        hence contradiction;

      end;

      hence thesis by Th1;

    end;

    theorem :: MATRIX_7:5

    

     Th5: for D be non empty set, f be FinSequence of D, k2 be Nat st 1 <= k2 & k2 < ( len f) holds f = (( mid (f,1,k2)) ^ ( mid (f,(k2 + 1),( len f))))

    proof

      let D be non empty set, f be FinSequence of D, k2 be Nat;

      assume

       A1: 1 <= k2 & k2 < ( len f);

      then ( mid (f,1,( len f))) = (( mid (f,1,k2)) ^ ( mid (f,(k2 + 1),( len f)))) by INTEGRA2: 4;

      hence thesis by A1, FINSEQ_6: 120, XXREAL_0: 2;

    end;

    theorem :: MATRIX_7:6

    

     Th6: for D be non empty set, f be FinSequence of D st 2 <= ( len f) holds f = ((f | (( len f) -' 2)) ^ ( mid (f,(( len f) -' 1),( len f))))

    proof

      let D be non empty set, f be FinSequence of D;

      assume

       A1: 2 <= ( len f);

      then

       A2: (( len f) -' 2) = (( len f) - 2) by XREAL_1: 233;

      

      then

       A3: ((( len f) -' 2) + 1) = (((( len f) - 1) - 1) + 1)

      .= (( len f) -' 1) by A1, XREAL_1: 233, XXREAL_0: 2;

      now

        per cases ;

          case (( len f) -' 2) > 0 ;

          then

           A4: ( 0 + 1) <= (( len f) -' 2) by NAT_1: 13;

          ( len f) < (( len f) + 1) by NAT_1: 13;

          then ( len f) < ((( len f) + 1) + 1) by NAT_1: 13;

          then (( len f) - 2) < ((( len f) + 2) - 2) by XREAL_1: 14;

          then f = (( mid (f,1,(( len f) -' 2))) ^ ( mid (f,((( len f) -' 2) + 1),( len f)))) by A2, A4, Th5;

          hence thesis by A3, A4, FINSEQ_6: 116;

        end;

          case

           A5: (( len f) -' 2) = 0 ;

          then

           A6: ( mid (f,((( len f) -' 2) + 1),( len f))) = f by A1, FINSEQ_6: 120, XXREAL_0: 2;

          

           A7: (f | 0 ) is empty;

          ((( len f) -' 2) + 1) = ((( len f) - 2) + 1) by A1, XREAL_1: 233

          .= (( len f) - 1)

          .= (( len f) -' 1) by A1, XREAL_1: 233, XXREAL_0: 2;

          hence thesis by A5, A6, A7, FINSEQ_1: 34;

        end;

      end;

      hence thesis;

    end;

    theorem :: MATRIX_7:7

    

     Th7: for D be non empty set, f be FinSequence of D st 1 <= ( len f) holds f = ((f | (( len f) -' 1)) ^ ( mid (f,( len f),( len f))))

    proof

      let D be non empty set, f be FinSequence of D;

      assume

       A1: 1 <= ( len f);

      then

       A2: (( len f) -' 1) = (( len f) - 1) by XREAL_1: 233;

      now

        per cases ;

          case (( len f) -' 1) > 0 ;

          then

           A3: ( 0 + 1) <= (( len f) -' 1) by NAT_1: 13;

          ( len f) < (( len f) + 1) by NAT_1: 13;

          then (( len f) - 1) < ((( len f) + 1) - 1) by XREAL_1: 14;

          then f = (( mid (f,1,(( len f) -' 1))) ^ ( mid (f,((( len f) -' 1) + 1),( len f)))) by A2, A3, Th5;

          hence thesis by A2, A3, FINSEQ_6: 116;

        end;

          case

           A4: (( len f) -' 1) = 0 ;

          

           A5: (f | 0 ) is empty;

          ( mid (f,((( len f) -' 1) + 1),( len f))) = f by A1, A4, FINSEQ_6: 120;

          hence thesis by A2, A4, A5, FINSEQ_1: 34;

        end;

      end;

      hence thesis;

    end;

    

     Lm1: <*1, 2*> <> <*2, 1*> by FINSEQ_1: 77;

    theorem :: MATRIX_7:8

    

     Th8: for a be Element of ( Group_of_Perm 2) st (ex q be Element of ( Permutations 2) st q = a & q is being_transposition) holds a = <*2, 1*>

    proof

      let a be Element of ( Group_of_Perm 2);

      given q be Element of ( Permutations 2) such that

       A1: q = a and

       A2: q is being_transposition;

      the carrier of ( Group_of_Perm 2) = ( Permutations 2) by MATRIX_1:def 13;

      then

      reconsider b = a as Permutation of ( Seg 2) by MATRIX_1:def 12;

      ex i,j be Nat st i in ( dom q) & j in ( dom q) & i <> j & (q . i) = j & (q . j) = i & for k be Nat st k <> i & k <> j & k in ( dom q) holds (q . k) = k by A2;

      then b is being_transposition by A1;

      hence thesis by Th4;

    end;

    theorem :: MATRIX_7:9

    for n be Nat, a,b be Element of ( Group_of_Perm n), pa,pb be Element of ( Permutations n) st a = pa & b = pb holds (a * b) = (pb * pa) by MATRIX_1:def 13;

    theorem :: MATRIX_7:10

    

     Th10: for a,b be Element of ( Group_of_Perm 2) st (ex p be Element of ( Permutations 2) st p = a & p is being_transposition) & (ex q be Element of ( Permutations 2) st q = b & q is being_transposition) holds (a * b) = <*1, 2*>

    proof

      let a,b be Element of ( Group_of_Perm 2);

      assume that

       A1: ex p be Element of ( Permutations 2) st p = a & p is being_transposition and

       A2: ex q be Element of ( Permutations 2) st q = b & q is being_transposition;

      consider p be Element of ( Permutations 2) such that

       A3: p = a and

       A4: p is being_transposition by A1;

      the carrier of ( Group_of_Perm 2) = ( Permutations 2) by MATRIX_1:def 13;

      then

       A5: (a * b) = <*1, 2*> or (a * b) = <*2, 1*> by Th3, TARSKI:def 2;

      reconsider p2 = p as FinSequence by A3, A4, Th8;

      

       A6: a = <*2, 1*> by A1, Th8;

      then ( len p2) = 2 by A3, FINSEQ_1: 44;

      then 1 in ( Seg ( len p2));

      then

       A7: 1 in ( dom p2) by FINSEQ_1:def 3;

      consider q be Element of ( Permutations 2) such that

       A8: q = b and

       A9: q is being_transposition by A2;

      reconsider q2 = q as FinSequence by A8, A9, Th8;

      b = <*2, 1*> by A2, Th8;

      then

       A10: (q2 . 2) = 1 by A8, FINSEQ_1: 44;

      

       A11: (a * b) = (q * p) by A3, A8, MATRIX_1:def 13;

      (p2 . 1) = 2 by A6, A3, FINSEQ_1: 44;

      then ((q * p) . 1) = 1 by A10, A7, FUNCT_1: 13;

      hence thesis by A5, A11, FINSEQ_1: 44;

    end;

    theorem :: MATRIX_7:11

    

     Th11: for l be FinSequence of ( Group_of_Perm 2) st (( len l) mod 2) = 0 & (for i st i in ( dom l) holds (ex q be Element of ( Permutations 2) st (l . i) = q & q is being_transposition)) holds ( Product l) = <*1, 2*>

    proof

      defpred P[ Nat] means for f be FinSequence of ( Group_of_Perm 2) st ( len f) = (2 * $1) & (for i st i in ( dom f) holds (ex q be Element of ( Permutations 2) st (f . i) = q & q is being_transposition)) holds ( Product f) = <*1, 2*>;

      let l be FinSequence of ( Group_of_Perm 2);

      assume that

       A1: (( len l) mod 2) = 0 and

       A2: for i st i in ( dom l) holds ex q be Element of ( Permutations 2) st (l . i) = q & q is being_transposition;

      (ex t be Nat st ( len l) = ((2 * t) + 0 ) & 0 < 2) or 0 = 0 & 2 = 0 by A1, NAT_D:def 2;

      then

      consider t be Nat such that

       A3: ( len l) = (2 * t);

      

       A4: for s be Nat st P[s] holds P[(s + 1)]

      proof

        let s be Nat;

        assume

         A5: P[s];

        for f be FinSequence of ( Group_of_Perm 2) st ( len f) = (2 * (s + 1)) & (for i st i in ( dom f) holds (ex q be Element of ( Permutations 2) st (f . i) = q & q is being_transposition)) holds ( Product f) = <*1, 2*>

        proof

          let f be FinSequence of ( Group_of_Perm 2);

          assume that

           A6: ( len f) = (2 * (s + 1)) and

           A7: for i st i in ( dom f) holds ex q be Element of ( Permutations 2) st (f . i) = q & q is being_transposition;

          

           A8: ( len f) = ((2 * s) + 2) by A6;

          then

           A9: 2 <= ( len f) by NAT_1: 11;

          then

           A10: (( len f) -' 1) = (( len f) - 1) by XREAL_1: 233, XXREAL_0: 2;

          

           A11: ((( len f) - (( len f) -' 1)) + 1) = ((( len f) - (( len f) - 1)) + 1) by A9, XREAL_1: 233, XXREAL_0: 2

          .= 2;

          set g = ( mid (f,(( len f) -' 1),( len f)));

          

           A12: (( len f) -' 1) <= ( len f) by NAT_D: 35;

          

           A13: 1 <= ( len f) by A9, XXREAL_0: 2;

          then ( len f) in ( Seg ( len f));

          then ( len f) in ( dom f) by FINSEQ_1:def 3;

          then

           A14: ex q be Element of ( Permutations 2) st (f . ( len f)) = q & q is being_transposition by A7;

          reconsider pw2 = ( Product ( mid (g,( len g),( len g)))) as Element of ( Group_of_Perm 2);

          reconsider pw1 = ( Product (g | (( len g) -' 1))) as Element of ( Group_of_Perm 2);

          

           A15: ((1 + (( len f) -' 1)) -' 1) = ((1 + (( len f) -' 1)) - 1) by NAT_1: 11, XREAL_1: 233

          .= (( len f) -' 1);

          

           A16: ((1 + 1) - 1) <= (( len f) - 1) by A9, XREAL_1: 13;

          then

           A17: 1 <= (( len f) -' 1) by A9, XREAL_1: 233, XXREAL_0: 2;

          

          then

           A18: ( len ( mid (f,(( len f) -' 1),( len f)))) = ((( len f) -' (( len f) -' 1)) + 1) by A13, A12, FINSEQ_6: 118

          .= ((( len f) - (( len f) -' 1)) + 1) by NAT_D: 35, XREAL_1: 233

          .= ((( len f) - (( len f) - 1)) + 1) by A9, XREAL_1: 233, XXREAL_0: 2

          .= 2;

          then (( len g) -' 1) = (( len g) - 1) by XREAL_1: 233;

          

          then

           A19: ((g | (( len g) -' 1)) . 1) = (g . 1) by A18, FINSEQ_3: 112

          .= (f . (( len f) -' 1)) by A16, A12, A11, A15, FINSEQ_6: 122;

          

           A20: for i st i in ( dom (f | (( len f) -' 2))) holds ex q be Element of ( Permutations 2) st ((f | (( len f) -' 2)) . i) = q & q is being_transposition

          proof

            let i;

            assume i in ( dom (f | (( len f) -' 2)));

            then

             A21: i in ( Seg ( len (f | (( len f) -' 2)))) by FINSEQ_1:def 3;

            then

             A22: 1 <= i by FINSEQ_1: 1;

            

             A23: i <= ( len (f | (( len f) -' 2))) by A21, FINSEQ_1: 1;

            ( len (f | (( len f) -' 2))) <= ( len f) by FINSEQ_5: 16;

            then i <= ( len f) by A23, XXREAL_0: 2;

            then i in ( dom f) by A22, FINSEQ_3: 25;

            then

             A24: ex q be Element of ( Permutations 2) st (f . i) = q & q is being_transposition by A7;

            ( len (f | (( len f) -' 2))) = (( len f) -' 2) by FINSEQ_1: 59, NAT_D: 35;

            hence thesis by A23, A24, FINSEQ_3: 112;

          end;

          ( len (f | (( len f) -' 2))) = (( len f) -' 2) by FINSEQ_1: 59, NAT_D: 35

          .= (2 * s) by A8, NAT_D: 34;

          then ( Product (f | (( len f) -' 2))) = <*1, 2*> by A5, A20;

          then

           A25: ( 1_ ( Group_of_Perm 2)) = ( Product (f | (( len f) -' 2))) by FINSEQ_2: 52, MATRIX_1: 15;

          f = ((f | (( len f) -' 2)) ^ ( mid (f,(( len f) -' 1),( len f)))) by A8, Th6, NAT_1: 11;

          

          then

           A26: ( Product f) = (( Product (f | (( len f) -' 2))) * ( Product ( mid (f,(( len f) -' 1),( len f))))) by GROUP_4: 5

          .= ( Product ( mid (f,(( len f) -' 1),( len f)))) by A25, GROUP_1:def 4;

          2 <= (2 + (( len f) -' 1)) by NAT_1: 11;

          

          then

           A27: ((2 + (( len f) -' 1)) -' 1) = ((2 + (( len f) -' 1)) - 1) by XREAL_1: 233, XXREAL_0: 2

          .= ( len f) by A10;

          

           A28: ((( len f) - (( len f) -' 1)) + 1) = ((( len f) - (( len f) - 1)) + 1) by A9, XREAL_1: 233, XXREAL_0: 2

          .= (1 + 1);

          

           A29: ((1 + ( len g)) -' 1) = ((1 + ( len g)) - 1) by NAT_1: 11, XREAL_1: 233;

          

           A30: ( len (g | (( len g) -' 1))) = (( len g) -' 1) by FINSEQ_1: 59, NAT_D: 35

          .= (( len g) - 1) by A18, XREAL_1: 233

          .= 1 by A18;

          then 1 in ( Seg ( len (g | (( len g) -' 1))));

          then 1 in ( dom (g | (( len g) -' 1))) by FINSEQ_1:def 3;

          then ( rng (g | (( len g) -' 1))) c= the carrier of ( Group_of_Perm 2) & ((g | (( len g) -' 1)) . 1) in ( rng (g | (( len g) -' 1))) by FINSEQ_1:def 4, FUNCT_1:def 3;

          then

          reconsider r = ((g | (( len g) -' 1)) . 1) as Element of ( Group_of_Perm 2);

          

           A31: pw1 = ( Product <*r*>) by A30, FINSEQ_1: 40

          .= (f . (( len f) -' 1)) by A19, FINSOP_1: 11;

          1 <= ((( len g) - ( len g)) + 1);

          

          then

           A32: (( mid (g,( len g),( len g))) . 1) = (g . ((1 + ( len g)) -' 1)) by A18, FINSEQ_6: 122

          .= (f . ( len f)) by A16, A12, A18, A28, A29, A27, FINSEQ_6: 122;

          

           A33: ( len ( mid (g,( len g),( len g)))) = ((( len g) -' ( len g)) + 1) by A18, FINSEQ_6: 118

          .= ( 0 + 1) by XREAL_1: 232

          .= 1;

          then 1 in ( Seg ( len ( mid (g,( len g),( len g)))));

          then 1 in ( dom ( mid (g,( len g),( len g)))) by FINSEQ_1:def 3;

          then ( rng ( mid (g,( len g),( len g)))) c= the carrier of ( Group_of_Perm 2) & (( mid (g,( len g),( len g))) . 1) in ( rng ( mid (g,( len g),( len g)))) by FINSEQ_1:def 4, FUNCT_1:def 3;

          then

          reconsider s = (( mid (g,( len g),( len g))) . 1) as Element of ( Group_of_Perm 2);

          

           A34: pw2 = ( Product <*s*>) by A33, FINSEQ_1: 40

          .= (f . ( len f)) by A32, FINSOP_1: 11;

          (( len f) -' 1) in ( Seg ( len f)) by A17, A12;

          then (( len f) -' 1) in ( dom f) by FINSEQ_1:def 3;

          then

           A35: ex q be Element of ( Permutations 2) st (f . (( len f) -' 1)) = q & q is being_transposition by A7;

          g = ((g | (( len g) -' 1)) ^ ( mid (g,( len g),( len g)))) by A18, Th7;

          

          then ( Product g) = (( Product (g | (( len g) -' 1))) * ( Product ( mid (g,( len g),( len g))))) by GROUP_4: 5

          .= <*1, 2*> by A35, A14, A31, A34, Th10;

          hence thesis by A26;

        end;

        hence thesis;

      end;

      for f be FinSequence of ( Group_of_Perm 2) st ( len f) = (2 * 0 ) & (for i st i in ( dom f) holds (ex q be Element of ( Permutations 2) st (f . i) = q & q is being_transposition)) holds ( Product f) = <*1, 2*>

      proof

        set G = ( Group_of_Perm 2);

        let f be FinSequence of ( Group_of_Perm 2);

        assume that

         A36: ( len f) = (2 * 0 ) and for i st i in ( dom f) holds ex q be Element of ( Permutations 2) st (f . i) = q & q is being_transposition;

        

         A37: ( 1_ G) = <*1, 2*> by FINSEQ_2: 52, MATRIX_1: 15;

        f = ( <*> the carrier of G) by A36;

        hence thesis by A37, GROUP_4: 8;

      end;

      then

       A38: P[ 0 ];

      

       A39: for s be Nat holds P[s] from NAT_1:sch 2( A38, A4);

      reconsider t as Nat;

      ( len l) = (2 * t) by A3;

      hence thesis by A2, A39;

    end;

    theorem :: MATRIX_7:12

    for K be Field, M be Matrix of 2, K holds ( Det M) = (((M * (1,1)) * (M * (2,2))) - ((M * (1,2)) * (M * (2,1))))

    proof

      reconsider s1 = <*1, 2*>, s2 = <*2, 1*> as Permutation of ( Seg 2) by Th2;

      let K be Field, M be Matrix of 2, K;

       A1:

      now

        

         A2: (s1 . 1) = 1 by FINSEQ_1: 44;

        assume s1 = s2;

        hence contradiction by A2, FINSEQ_1: 44;

      end;

      set D0 = {s1, s2};

      reconsider l0 = ( <*> D0) as FinSequence of ( Group_of_Perm 2) by Th3, MATRIX_1:def 13;

      set X = ( Permutations 2);

      reconsider p1 = s1, p2 = s2 as Element of ( Permutations 2) by MATRIX_1:def 12;

      set Y = the carrier of K;

      set f = ( Path_product M);

      set F = the addF of K;

      set di = (the multF of K $$ ( Path_matrix (p1,M)));

      set B = ( In (( Permutations 2),( Fin ( Permutations 2))));

      ( Permutations 2) in ( Fin ( Permutations 2)) by FINSUB_1:def 5;

      then

       A3: B = ( Permutations 2) by SUBSET_1:def 8;

      ( Det M) = (the addF of K $$ (( In (( Permutations 2),( Fin ( Permutations 2)))),( Path_product M))) by MATRIX_3:def 9;

      then

      consider G be Function of ( Fin X), Y such that

       A4: ( Det M) = (G . B) and for e be Element of Y st e is_a_unity_wrt F holds (G . {} ) = e and

       A5: for x be Element of X holds (G . {x}) = (f . x) and

       A6: for B9 be Element of ( Fin X) st B9 c= B & B9 <> {} holds for x be Element of X st x in (B \ B9) holds (G . (B9 \/ {x})) = (F . ((G . B9),(f . x))) by A3, SETWISEO:def 3;

      

       A7: (G . {p1}) = (f . p1) by A5;

      

       A8: (G . B) = (the addF of K . ((f . p1),(f . p2)))

      proof

        reconsider B9 = {.p1.} as Element of ( Fin X);

        

         A9: B9 c= B

        proof

          let y be object;

          assume y in B9;

          then y = p1 by TARSKI:def 1;

          hence thesis by A3;

        end;

        (B \ B9) = {s2} by A1, A3, Th3, ZFMISC_1: 17;

        then s2 in (B \ B9) by TARSKI:def 1;

        then (G . (B9 \/ {p2})) = (F . ((G . B9),(f . p2))) by A6, A9;

        hence thesis by A3, A7, Th3, ENUMSET1: 1;

      end;

      set dj = (the multF of K $$ ( Path_matrix (p2,M)));

      

       A10: (p1 . 2) = 2 by FINSEQ_1: 44;

      

       A11: (p2 . 2) = 1 by FINSEQ_1: 44;

      

       A12: ( len ( Path_matrix (p1,M))) = 2 by MATRIX_3:def 7;

      then

      consider f3 be sequence of the carrier of K such that

       A13: (f3 . 1) = (( Path_matrix (p1,M)) . 1) and

       A14: for n be Nat st 0 <> n & n < 2 holds (f3 . (n + 1)) = (the multF of K . ((f3 . n),(( Path_matrix (p1,M)) . (n + 1)))) and

       A15: di = (f3 . 2) by FINSOP_1:def 1;

      

       A16: 1 in ( Seg 2);

      then

       A17: 1 in ( dom ( Path_matrix (p1,M))) by A12, FINSEQ_1:def 3;

      

       A18: 2 in ( Seg 2);

      then 2 in ( dom ( Path_matrix (p1,M))) by A12, FINSEQ_1:def 3;

      then

       A19: (p1 . 1) = 1 & (( Path_matrix (p1,M)) . 2) = (M * (2,2)) by A10, FINSEQ_1: 44, MATRIX_3:def 7;

      

       A20: ( len ( Path_matrix (p2,M))) = 2 by MATRIX_3:def 7;

      then

      consider f4 be sequence of the carrier of K such that

       A21: (f4 . 1) = (( Path_matrix (p2,M)) . 1) and

       A22: for n be Nat st 0 <> n & n < 2 holds (f4 . (n + 1)) = (the multF of K . ((f4 . n),(( Path_matrix (p2,M)) . (n + 1)))) and

       A23: dj = (f4 . 2) by FINSOP_1:def 1;

      

       A24: 1 in ( dom ( Path_matrix (p2,M))) by A20, A16, FINSEQ_1:def 3;

      2 in ( dom ( Path_matrix (p2,M))) by A20, A18, FINSEQ_1:def 3;

      then

       A25: (p2 . 1) = 2 & (( Path_matrix (p2,M)) . 2) = (M * (2,1)) by A11, FINSEQ_1: 44, MATRIX_3:def 7;

      

       A26: (f4 . (1 + 1)) = (the multF of K . ((f4 . 1),(( Path_matrix (p2,M)) . (1 + 1)))) by A22

      .= ((M * (1,2)) * (M * (2,1))) by A24, A25, A21, MATRIX_3:def 7;

      

       A27: ( len ( Permutations 2)) = 2 by MATRIX_1: 9;

       not ex l be FinSequence of ( Group_of_Perm 2) st (( len l) mod 2) = 0 & s2 = ( Product l) & for i st i in ( dom l) holds ex q be Element of ( Permutations 2) st (l . i) = q & q is being_transposition by Lm1, Th11;

      then (f . p2) = ( - ((the multF of K "**" ( Path_matrix (p2,M))),p2)) & p2 is odd by A27, MATRIX_3:def 8;

      then

       A28: (f . p2) = ( - dj) by MATRIX_1:def 16;

      

       A29: ( Product l0) = ( Product ( <*> the carrier of ( Group_of_Perm 2)))

      .= ( 1_ ( Group_of_Perm 2)) by GROUP_4: 8

      .= p1 by FINSEQ_2: 52, MATRIX_1: 15;

      

       A30: ( 0 mod 2) = 0 by NAT_D: 26;

      ex l be FinSequence of ( Group_of_Perm 2) st (( len l) mod 2) = 0 & s1 = ( Product l) & for i st i in ( dom l) holds ex q be Element of ( Permutations 2) st (l . i) = q & q is being_transposition

      proof

        take l0;

        thus (( len l0) mod 2) = 0 & s1 = ( Product l0) by A30, A29;

        let i;

        thus thesis;

      end;

      then

       A31: (f . p1) = ( - ((the multF of K "**" ( Path_matrix (p1,M))),p1)) & p1 is even by A27, MATRIX_3:def 8;

      (f3 . (1 + 1)) = (the multF of K . ((f3 . 1),(( Path_matrix (p1,M)) . (1 + 1)))) by A14

      .= ((M * (1,1)) * (M * (2,2))) by A17, A19, A13, MATRIX_3:def 7;

      hence thesis by A4, A8, A15, A23, A26, A31, A28, MATRIX_1:def 16;

    end;

    definition

      let n be Nat, K be commutative Ring;

      let M be Matrix of n, K, a be Element of K;

      :: original: *

      redefine

      func a * M -> Matrix of n, K ;

      coherence

      proof

        

         A1: ( width (a * M)) = ( width M) by MATRIX_3:def 5;

        

         A2: ( len M) = n by MATRIX_0:def 2;

        

         A3: ( len (a * M)) = ( len M) by MATRIX_3:def 5;

        

         A4: ( len M) = n by MATRIX_0:def 2;

        now

          per cases ;

            case

             A5: ( len M) > 0 ;

            then n = ( width M) by A2, MATRIX_0: 20;

            hence thesis by A2, A3, A1, A5, MATRIX_0: 20;

          end;

            case ( len M) <= 0 ;

            then

             A6: ( len (a * M)) = 0 by MATRIX_3:def 5;

            then

             A7: ( Seg ( len (a * M))) = {} ;

            for p be FinSequence of K st p in ( rng (a * M)) holds ( len p) = 0

            proof

              let p be FinSequence of K;

              assume p in ( rng (a * M));

              then ex x be object st x in ( dom (a * M)) & p = ((a * M) . x) by FUNCT_1:def 3;

              hence thesis by A7, FINSEQ_1:def 3;

            end;

            hence thesis by A4, A3, A6, MATRIX_0:def 2;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: MATRIX_7:13

    

     Th13: for K be Ring, n,m be Nat holds ( len ( 0. (K,n,m))) = n & ( dom ( 0. (K,n,m))) = ( Seg n)

    proof

      let K be Ring, n,m be Nat;

      ( len (n |-> (m |-> ( 0. K)))) = n by CARD_1:def 7;

      hence ( len ( 0. (K,n,m))) = n by MATRIX_3:def 1;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: MATRIX_7:14

    

     Th14: for K be Ring, n be Nat, p be Element of ( Permutations n), i be Nat st i in ( Seg n) holds (p . i) in ( Seg n)

    proof

      let K be Ring, n be Nat, p be Element of ( Permutations n), i be Nat;

      

       A1: p is Permutation of ( Seg n) by MATRIX_1:def 12;

      assume i in ( Seg n);

      hence thesis by A1, FUNCT_2: 5;

    end;

    theorem :: MATRIX_7:15

    for K be Ring, n be Nat st n >= 1 holds ( Det ( 0. (K,n,n))) = ( 0. K)

    proof

      let K be Ring, n be Nat;

      set B = ( In (( Permutations n),( Fin ( Permutations n))));

      set f = ( Path_product ( 0. (K,n,n)));

      set F = the addF of K;

      set Y = the carrier of K;

      set X = ( Permutations n);

      reconsider G0 = (( Fin X) --> ( 0. K)) as Function of ( Fin X), Y;

      

       A1: (G0 . B) = ( 0. K) by FUNCOP_1: 7;

      

       A2: for e be Element of Y st e is_a_unity_wrt F holds (G0 . {} ) = e

      proof

        let e be Element of Y;

        ( 0. K) is_a_unity_wrt F by FVSUM_1: 6;

        then

         A3: (F . (( 0. K),e)) = e by BINOP_1: 3;

        assume e is_a_unity_wrt F;

        then (F . (( 0. K),e)) = ( 0. K) by BINOP_1: 3;

        hence thesis by A3, FINSUB_1: 7, FUNCOP_1: 7;

      end;

      assume

       A4: n >= 1;

      

       A5: for x be object st x in ( dom ( Path_product ( 0. (K,n,n)))) holds (( Path_product ( 0. (K,n,n))) . x) = ((( Permutations n) --> ( 0. K)) . x)

      proof

        let x be object;

        assume x in ( dom ( Path_product ( 0. (K,n,n))));

        for p be Element of ( Permutations n) holds ((( Permutations n) --> ( 0. K)) . p) = ( - ((the multF of K $$ ( Path_matrix (p,( 0. (K,n,n))))),p))

        proof

          defpred P[ Nat] means (the multF of K $$ (($1 + 1) |-> ( 0. K))) = ( 0. K);

          let p be Element of ( Permutations n);

          

           A6: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            

             A7: (((k + 1) + 1) |-> ( 0. K)) = (((k + 1) |-> ( 0. K)) ^ <*( 0. K)*>) by FINSEQ_2: 60;

            assume P[k];

            

            then (the multF of K $$ (((k + 1) + 1) |-> ( 0. K))) = (( 0. K) * ( 0. K)) by A7, FINSOP_1: 4

            .= ( 0. K);

            hence thesis;

          end;

          (1 |-> ( 0. K)) = <*( 0. K)*> by FINSEQ_2: 59;

          then

           A8: P[ 0 ] by FINSOP_1: 11;

          

           A9: for k be Nat holds P[k] from NAT_1:sch 2( A8, A6);

           A10:

          now

            per cases ;

              case p is even;

              hence ( - (( 0. K),p)) = ( 0. K) by MATRIX_1:def 16;

            end;

              case not p is even;

              

              then ( - (( 0. K),p)) = ( - ( 0. K)) by MATRIX_1:def 16

              .= ( 0. K) by RLVECT_1: 12;

              hence ( - (( 0. K),p)) = ( 0. K);

            end;

          end;

          

           A11: for i, j st i in ( dom (n |-> ( 0. K))) & j = (p . i) holds ((n |-> ( 0. K)) . i) = (( 0. (K,n,n)) * (i,j))

          proof

            let i, j;

            assume that

             A12: i in ( dom (n |-> ( 0. K))) and

             A13: j = (p . i);

            

             A14: i in ( Seg n) by A12, FUNCOP_1: 13;

            then j in ( Seg n) by A13, Th14;

            then

             A15: j in ( Seg ( width ( 0. (K,n,n)))) by A4, MATRIX_0: 23;

            i in ( dom ( 0. (K,n,n))) by A14, Th13;

            then

             A16: [i, j] in ( Indices ( 0. (K,n,n))) by A15, ZFMISC_1:def 2;

            ((n |-> ( 0. K)) . i) = ( 0. K) by A14, FUNCOP_1: 7;

            hence thesis by A16, MATRIX_3: 1;

          end;

          ( len (n |-> ( 0. K))) = n by CARD_1:def 7;

          then

           A17: ( Path_matrix (p,( 0. (K,n,n)))) = (n |-> ( 0. K)) by A11, MATRIX_3:def 7;

          (n -' 1) = (n - 1) by A4, XREAL_1: 233;

          then

           A18: ((n -' 1) + 1) = n;

          ((( Permutations n) --> ( 0. K)) . p) = ( 0. K) by FUNCOP_1: 7;

          hence thesis by A17, A9, A18, A10;

        end;

        hence thesis by MATRIX_3:def 8;

      end;

      ( dom (( Permutations n) --> ( 0. K))) = ( Permutations n) by FUNCOP_1: 13;

      then ( dom ( Path_product ( 0. (K,n,n)))) = ( dom (( Permutations n) --> ( 0. K))) by FUNCT_2:def 1;

      then

       A19: ( Path_product ( 0. (K,n,n))) = (( Permutations n) --> ( 0. K)) by A5, FUNCT_1: 2;

      

       A20: for x be Element of X holds (G0 . {x}) = (f . x)

      proof

        let x be Element of X;

        (G0 . {.x.}) = ( 0. K) by FUNCOP_1: 7;

        hence thesis by A19, FUNCOP_1: 7;

      end;

      

       A21: for B9 be Element of ( Fin X) st B9 c= B & B9 <> {} holds for x be Element of X st x in (B \ B9) holds (G0 . (B9 \/ {x})) = (F . ((G0 . B9),(f . x)))

      proof

        let B9 be Element of ( Fin X);

        assume that B9 c= B and B9 <> {} ;

        thus for x be Element of X st x in (B \ B9) holds (G0 . (B9 \/ {x})) = (F . ((G0 . B9),(f . x)))

        proof

          let x be Element of X;

          assume x in (B \ B9);

          

           A22: (G0 . (B9 \/ {.x.})) = ( 0. K) & (G0 . B9) = ( 0. K) by FUNCOP_1: 7;

          (f . x) = ( 0. K) & ( 0. K) is_a_unity_wrt F by A19, FUNCOP_1: 7, FVSUM_1: 6;

          hence thesis by A22, BINOP_1: 3;

        end;

      end;

      X in ( Fin X) by FINSUB_1:def 5;

      then B = X by SUBSET_1:def 8;

      then B <> {} or F is having_a_unity;

      then (the addF of K $$ (( In (( Permutations n),( Fin ( Permutations n)))),( Path_product ( 0. (K,n,n))))) = ( 0. K) by A1, A2, A20, A21, SETWISEO:def 3;

      hence thesis by MATRIX_3:def 9;

    end;

    definition

      let x be object;

      let y be set;

      let a,b be object;

      :: MATRIX_7:def1

      func IFIN (x,y,a,b) -> object equals

      : Def1: a if x in y

      otherwise b;

      correctness ;

    end

    theorem :: MATRIX_7:16

    for K be Ring, n be Nat st n >= 1 holds ( Det ( 1. (K,n))) = ( 1_ K)

    proof

      let K be Ring, n be Nat;

      assume

       A1: n >= 1;

      deffunc F2( object) = ( IFEQ (( idseq n),$1,( 1_ K),( 0. K)));

      set X = ( Permutations n);

      set Y = the carrier of K;

      

       A2: for x be object st x in X holds F2(x) in Y;

      ex f2 be Function of X, Y st for x be object st x in X holds (f2 . x) = F2(x) from FUNCT_2:sch 2( A2);

      then

      consider f2 be Function of X, Y such that

       A3: for x be object st x in X holds (f2 . x) = F2(x);

      

       A4: ( id ( Seg n)) is even by MATRIX_1: 16;

      

       A5: for x be object st x in ( dom ( Path_product ( 1. (K,n)))) holds (( Path_product ( 1. (K,n))) . x) = (f2 . x)

      proof

        let x be object;

        assume x in ( dom ( Path_product ( 1. (K,n))));

        for p be Element of ( Permutations n) holds (f2 . p) = ( - ((the multF of K $$ ( Path_matrix (p,( 1. (K,n))))),p))

        proof

          defpred P[ Nat] means (the multF of K $$ (($1 + 1) |-> ( 1_ K))) = ( 1_ K);

          let p be Element of ( Permutations n);

          

           A6: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            

             A7: (((k + 1) + 1) |-> ( 1_ K)) = (((k + 1) |-> ( 1_ K)) ^ <*( 1_ K)*>) by FINSEQ_2: 60;

            assume P[k];

            

            then (the multF of K $$ (((k + 1) + 1) |-> ( 1_ K))) = (( 1_ K) * ( 1_ K)) by A7, FINSOP_1: 4

            .= ( 1_ K);

            hence thesis;

          end;

           A8:

          now

            per cases ;

              case p is even;

              hence ( - (( 0. K),p)) = ( 0. K) by MATRIX_1:def 16;

            end;

              case not p is even;

              

              then ( - (( 0. K),p)) = ( - ( 0. K)) by MATRIX_1:def 16

              .= ( 0. K) by RLVECT_1: 12;

              hence ( - (( 0. K),p)) = ( 0. K);

            end;

          end;

          (n -' 1) = (n - 1) by A1, XREAL_1: 233;

          then

           A9: ((n -' 1) + 1) = n;

          (1 |-> ( 1_ K)) = <*( 1_ K)*> by FINSEQ_2: 59;

          then

           A10: P[ 0 ] by FINSOP_1: 11;

          for k be Nat holds P[k] from NAT_1:sch 2( A10, A6);

          then

           A11: ( len (n |-> ( 1_ K))) = n & (the multF of K $$ (n |-> ( 1_ K))) = ( 1_ K) by A9, CARD_1:def 7;

          now

            per cases ;

              case

               A12: p = ( idseq n);

              

               A13: for i, j st i in ( dom (n |-> ( 1_ K))) & j = (p . i) holds ((n |-> ( 1_ K)) . i) = (( 1. (K,n)) * (i,j))

              proof

                

                 A14: ( Indices ( 1. (K,n))) = [:( Seg n), ( Seg n):] by A1, MATRIX_0: 23;

                let i, j;

                assume that

                 A15: i in ( dom (n |-> ( 1_ K))) and

                 A16: j = (p . i);

                

                 A17: i in ( Seg n) by A15, FUNCOP_1: 13;

                then j in ( Seg n) by A16, Th14;

                then

                 A18: [i, j] in ( Indices ( 1. (K,n))) by A17, A14, ZFMISC_1:def 2;

                ((n |-> ( 1_ K)) . i) = ( 1_ K) & (p . i) = i by A12, A17, FUNCOP_1: 7, FUNCT_1: 17;

                hence thesis by A16, A18, MATRIX_1:def 3;

              end;

              ( len ( Permutations n)) = n by MATRIX_1: 9;

              then

               A19: ( - ((the multF of K $$ ( Path_matrix (p,( 1. (K,n))))),p)) = (the multF of K $$ ( Path_matrix (p,( 1. (K,n))))) by A4, A12, MATRIX_1:def 16;

              (f2 . p) = F2(p) by A3

              .= ( 1_ K) by A12, FUNCOP_1:def 8;

              hence thesis by A11, A19, A13, MATRIX_3:def 7;

            end;

              case

               A20: p <> ( idseq n);

              reconsider A = NAT as non empty set;

              defpred P3[ Nat] means $1 < n implies ex p3 be FinSequence of K st ( len p3) = ($1 + 1) & (p3 . 1) = (( Path_matrix (p,( 1. (K,n)))) . 1) & (for n3 be Nat st 0 <> n3 & n3 < ($1 + 1) & n3 < n holds (p3 . (n3 + 1)) = (the multF of K . ((p3 . n3),(( Path_matrix (p,( 1. (K,n)))) . (n3 + 1)))));

              

               A21: ( rng ( Path_matrix (p,( 1. (K,n))))) c= the carrier of K by FINSEQ_1:def 4;

              

               A22: ( len ( Path_matrix (p,( 1. (K,n))))) = n by MATRIX_3:def 7;

              then 1 in ( Seg ( len ( Path_matrix (p,( 1. (K,n)))))) by A1;

              then 1 in ( dom ( Path_matrix (p,( 1. (K,n))))) by FINSEQ_1:def 3;

              then (( Path_matrix (p,( 1. (K,n)))) . 1) in ( rng ( Path_matrix (p,( 1. (K,n))))) by FUNCT_1:def 3;

              then

              reconsider d = (( Path_matrix (p,( 1. (K,n)))) . 1) as Element of K by A21;

              reconsider q3 = <*d*> as FinSequence of K;

              

               A23: for n3 be Nat st 0 <> n3 & n3 < ( 0 + 1) & n3 < n holds (q3 . (n3 + 1)) = (the multF of K . ((q3 . n3),(( Path_matrix (p,( 1. (K,n)))) . (n3 + 1)))) by NAT_1: 13;

              

               A24: ( dom p) = ( Seg ( len ( Permutations n))) by FUNCT_2: 52;

              then

               A25: ( dom p) = ( Seg n) by MATRIX_1: 9;

              then ( dom p) = ( dom ( idseq n)) by RELAT_1: 45;

              then

              consider i0 be object such that

               A26: i0 in ( dom p) and

               A27: (p . i0) <> (( idseq n) . i0) by A20, FUNCT_1: 2;

              reconsider i0 as Element of NAT by A24, A26;

              

               A28: (p . i0) <> i0 by A25, A26, A27, FUNCT_1: 18;

              

               A29: for k be Nat st P3[k] holds P3[(k + 1)]

              proof

                let k be Nat;

                assume

                 A30: P3[k];

                now

                  per cases ;

                    case

                     A31: (k + 1) < n;

                    then

                    consider p3 be FinSequence of K such that

                     A32: ( len p3) = (k + 1) and

                     A33: (p3 . 1) = (( Path_matrix (p,( 1. (K,n)))) . 1) and

                     A34: for n3 be Nat st 0 <> n3 & n3 < (k + 1) & n3 < n holds (p3 . (n3 + 1)) = (the multF of K . ((p3 . n3),(( Path_matrix (p,( 1. (K,n)))) . (n3 + 1)))) by A30, NAT_1: 12;

                    defpred P6[ object, object] means ($1 in ( Seg (k + 1)) implies $2 = (p3 . $1)) & ( not $1 in ( Seg (k + 1)) implies $2 = ( 0. K));

                    

                     A35: for x be object st x in NAT holds ex y be object st y in the carrier of K & P6[x, y]

                    proof

                      let x be object;

                      assume x in NAT ;

                      now

                        per cases ;

                          case

                           A36: x in ( Seg (k + 1));

                          then

                          reconsider nx = x as Nat;

                          nx in ( dom p3) by A32, A36, FINSEQ_1:def 3;

                          then

                           A37: (p3 . nx) in ( rng p3) by FUNCT_1:def 3;

                          ( rng p3) c= the carrier of K by FINSEQ_1:def 4;

                          then

                          reconsider s = (p3 . nx) as Element of K by A37;

                          x in ( Seg (k + 1)) implies s = (p3 . x);

                          hence thesis by A36;

                        end;

                          case not x in ( Seg (k + 1));

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                    ex f6 be sequence of the carrier of K st for x be object st x in NAT holds P6[x, (f6 . x)] from FUNCT_2:sch 1( A35);

                    then

                    consider f6 be sequence of the carrier of K such that

                     A38: for x be object st x in NAT holds P6[x, (f6 . x)];

                    1 <= ((k + 1) + 1) & ((k + 1) + 1) <= n by A31, NAT_1: 12, NAT_1: 13;

                    then ((k + 1) + 1) in ( Seg ( len ( Path_matrix (p,( 1. (K,n)))))) by A22;

                    then ((k + 1) + 1) in ( dom ( Path_matrix (p,( 1. (K,n))))) by FINSEQ_1:def 3;

                    then ( rng ( Path_matrix (p,( 1. (K,n))))) c= the carrier of K & (( Path_matrix (p,( 1. (K,n)))) . ((k + 1) + 1)) in ( rng ( Path_matrix (p,( 1. (K,n))))) by FINSEQ_1:def 4, FUNCT_1:def 3;

                    then [(f6 . (k + 1)), (( Path_matrix (p,( 1. (K,n)))) . ((k + 1) + 1))] in [:the carrier of K, the carrier of K:] by ZFMISC_1:def 2;

                    then

                    reconsider e = (the multF of K . ((f6 . (k + 1)),(( Path_matrix (p,( 1. (K,n)))) . ((k + 1) + 1)))) as Element of K by FUNCT_2: 5;

                    reconsider q3 = (p3 ^ <*e*>) as FinSequence of K;

                    

                     A39: ( len q3) = (( len p3) + ( len <*e*>)) by FINSEQ_1: 22

                    .= ((k + 1) + 1) by A32, FINSEQ_1: 40;

                    

                     A40: for n3 be Nat st 0 <> n3 & n3 < ((k + 1) + 1) & n3 < n holds (q3 . (n3 + 1)) = (the multF of K . ((q3 . n3),(( Path_matrix (p,( 1. (K,n)))) . (n3 + 1))))

                    proof

                      let n3 be Nat;

                      assume that

                       A41: 0 <> n3 and

                       A42: n3 < ((k + 1) + 1) and

                       A43: n3 < n;

                      now

                        per cases ;

                          case

                           A44: n3 < (k + 1);

                          then 1 <= (n3 + 1) & (n3 + 1) <= (k + 1) by NAT_1: 12, NAT_1: 13;

                          then (n3 + 1) in ( Seg ( len p3)) by A32;

                          then (n3 + 1) in ( dom p3) by FINSEQ_1:def 3;

                          then

                           A45: (p3 . (n3 + 1)) = (q3 . (n3 + 1)) by FINSEQ_1:def 7;

                          ( 0 + 1) <= n3 by A41, NAT_1: 13;

                          then n3 in ( Seg ( len p3)) by A32, A44;

                          then

                           A46: n3 in ( dom p3) by FINSEQ_1:def 3;

                          (p3 . (n3 + 1)) = (the multF of K . ((p3 . n3),(( Path_matrix (p,( 1. (K,n)))) . (n3 + 1)))) by A34, A41, A43, A44;

                          hence thesis by A45, A46, FINSEQ_1:def 7;

                        end;

                          case

                           A47: n3 >= (k + 1);

                          

                           A48: (n3 + 1) <= ((k + 1) + 1) by A42, NAT_1: 13;

                          

                           A49: (n3 + 1) > (k + 1) by A47, NAT_1: 13;

                          then (n3 + 1) >= ((k + 1) + 1) by NAT_1: 13;

                          then

                           A50: (n3 + 1) = ((k + 1) + 1) by A48, XXREAL_0: 1;

                          1 <= (k + 1) by NAT_1: 12;

                          then

                           A51: (k + 1) in ( Seg (k + 1));

                          then (k + 1) in ( dom p3) by A32, FINSEQ_1:def 3;

                          then

                           A52: (q3 . (k + 1)) = (p3 . (k + 1)) by FINSEQ_1:def 7;

                          (q3 . (n3 + 1)) = ( <*e*> . ((n3 + 1) - (k + 1))) by A32, A39, A49, A48, FINSEQ_1: 24

                          .= e by A50, FINSEQ_1:def 8;

                          hence thesis by A38, A50, A51, A52;

                        end;

                      end;

                      hence thesis;

                    end;

                    1 <= (k + 1) by NAT_1: 12;

                    then 1 in ( Seg ( len p3)) by A32;

                    then 1 in ( dom p3) by FINSEQ_1:def 3;

                    then (q3 . 1) = (( Path_matrix (p,( 1. (K,n)))) . 1) by A33, FINSEQ_1:def 7;

                    hence thesis by A39, A40;

                  end;

                    case (k + 1) >= n;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

              n < (n + 1) by NAT_1: 13;

              then

               A53: (n - 1) < ((n + 1) - 1) by XREAL_1: 14;

              

               A54: (f2 . p) = F2(p) by A3

              .= ( 0. K) by A20, FUNCOP_1:def 8;

              

               A55: (n - 1) = (n -' 1) by A1, XREAL_1: 233;

              ( len q3) = 1 & (q3 . 1) = (( Path_matrix (p,( 1. (K,n)))) . 1) by FINSEQ_1: 40;

              then

               A56: P3[ 0 ] by A23;

              for k be Nat holds P3[k] from NAT_1:sch 2( A56, A29);

              then

              consider p3 be FinSequence of K such that

               A57: ( len p3) = ((n -' 1) + 1) and

               A58: (p3 . 1) = (( Path_matrix (p,( 1. (K,n)))) . 1) and

               A59: for n3 be Nat st 0 <> n3 & n3 < ((n -' 1) + 1) & n3 < n holds (p3 . (n3 + 1)) = (the multF of K . ((p3 . n3),(( Path_matrix (p,( 1. (K,n)))) . (n3 + 1)))) by A55, A53;

              defpred P[ set, set] means ($1 in ( Seg n) implies $2 = (p3 . $1)) & ( not $1 in ( Seg n) implies $2 = ( 0. K));

              

               A60: for x3 be Element of A holds ex y3 be Element of K st P[x3, y3]

              proof

                let x3 be Element of A;

                now

                  per cases ;

                    case

                     A61: x3 in ( Seg n);

                    then x3 in ( dom p3) by A55, A57, FINSEQ_1:def 3;

                    then ( rng p3) c= the carrier of K & (p3 . x3) in ( rng p3) by FINSEQ_1:def 4, FUNCT_1:def 3;

                    hence thesis by A61;

                  end;

                    case not x3 in ( Seg n);

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

              ex f4 be Function of A, the carrier of K st for x2 be Element of A holds P[x2, (f4 . x2)] from FUNCT_2:sch 3( A60);

              then

              consider f4 be sequence of the carrier of K such that

               A62: for x4 be Element of NAT holds (x4 in ( Seg n) implies (f4 . x4) = (p3 . x4)) & ( not x4 in ( Seg n) implies (f4 . x4) = ( 0. K));

              p is Permutation of ( Seg n) by MATRIX_1:def 12;

              then

               A63: (p . i0) in ( Seg n) by A25, A26, FUNCT_2: 5;

              then

              reconsider j0 = (p . i0) as Element of NAT ;

              ( Indices ( 1. (K,n))) = [:( Seg n), ( Seg n):] by A1, MATRIX_0: 23;

              then

               A64: [i0, j0] in ( Indices ( 1. (K,n))) by A25, A26, A63, ZFMISC_1:def 2;

              i0 <= n by A25, A26, FINSEQ_1: 1;

              then

               A65: (n -' i0) = (n - i0) by XREAL_1: 233;

              i0 in ( dom ( Path_matrix (p,( 1. (K,n))))) by A25, A26, A22, FINSEQ_1:def 3;

              then

               A66: (( Path_matrix (p,( 1. (K,n)))) . i0) = (( 1. (K,n)) * (i0,j0)) by MATRIX_3:def 7;

              defpred P5[ Nat] means (f4 . (i0 + $1)) = ( 0. K);

              

               A67: 0 < i0 by A24, A26, FINSEQ_1: 1;

              

               A68: for k be Nat st P5[k] holds P5[(k + 1)]

              proof

                let k be Nat;

                

                 A69: 1 <= (1 + (i0 + k)) by NAT_1: 12;

                assume

                 A70: P5[k];

                now

                  per cases ;

                    case

                     A71: ((i0 + k) + 1) <= n;

                    1 <= (1 + (i0 + k)) by NAT_1: 12;

                    then ((i0 + k) + 1) in ( Seg ( len ( Path_matrix (p,( 1. (K,n)))))) by A22, A71;

                    then ((i0 + k) + 1) in ( dom ( Path_matrix (p,( 1. (K,n))))) by FINSEQ_1:def 3;

                    then

                     A72: (( Path_matrix (p,( 1. (K,n)))) . ((i0 + k) + 1)) in ( rng ( Path_matrix (p,( 1. (K,n))))) by FUNCT_1:def 3;

                    ( rng ( Path_matrix (p,( 1. (K,n))))) c= the carrier of K by FINSEQ_1:def 4;

                    then

                    reconsider b = (( Path_matrix (p,( 1. (K,n)))) . ((i0 + k) + 1)) as Element of K by A72;

                    

                     A73: (i0 + k) < n by A71, NAT_1: 13;

                    ( 0 + 1) <= (i0 + k) by A67, NAT_1: 13;

                    then

                     A74: (i0 + k) in ( Seg n) by A73;

                    ((i0 + k) + 1) in ( Seg n) by A69, A71;

                    

                    then (f4 . ((i0 + k) + 1)) = (p3 . ((i0 + k) + 1)) by A62

                    .= (the multF of K . ((p3 . (i0 + k)),(( Path_matrix (p,( 1. (K,n)))) . ((i0 + k) + 1)))) by A55, A59, A67, A73

                    .= (( 0. K) * b) by A62, A70, A74

                    .= ( 0. K);

                    hence thesis;

                  end;

                    case ((i0 + k) + 1) > n;

                    then not (i0 + (k + 1)) in ( Seg n) by FINSEQ_1: 1;

                    hence thesis by A62;

                  end;

                end;

                hence thesis;

              end;

              1 in ( Seg n) by A1;

              then

               A75: (f4 . 1) = (( Path_matrix (p,( 1. (K,n)))) . 1) by A58, A62;

              

               A76: for n3 be Nat st 0 <> n3 & n3 < ( len ( Path_matrix (p,( 1. (K,n))))) holds (f4 . (n3 + 1)) = (the multF of K . ((f4 . n3),(( Path_matrix (p,( 1. (K,n)))) . (n3 + 1))))

              proof

                let n3 be Nat;

                assume that

                 A77: 0 <> n3 and

                 A78: n3 < ( len ( Path_matrix (p,( 1. (K,n)))));

                

                 A79: (n3 + 1) <= ( len ( Path_matrix (p,( 1. (K,n))))) by A78, NAT_1: 13;

                

                 A80: ( 0 + 1) <= n3 by A77, NAT_1: 13;

                then

                 A81: n3 in ( Seg n) by A22, A78;

                1 < (n3 + 1) by A80, NAT_1: 13;

                then (n3 + 1) in ( Seg n) by A22, A79;

                then

                 A82: (f4 . (n3 + 1)) = (p3 . (n3 + 1)) by A62;

                (p3 . (n3 + 1)) = (the multF of K . ((p3 . n3),(( Path_matrix (p,( 1. (K,n)))) . (n3 + 1)))) by A22, A55, A59, A77, A78;

                hence thesis by A62, A82, A81;

              end;

              

               A83: 1 <= i0 by A24, A26, FINSEQ_1: 1;

              now

                per cases ;

                  case i0 <= 1;

                  then i0 = 1 by A83, XXREAL_0: 1;

                  hence P5[ 0 ] by A28, A66, A64, A75, MATRIX_1:def 3;

                end;

                  case

                   A84: i0 > 1;

                  reconsider a = (f4 . (i0 -' 1)) as Element of K;

                  i0 < (i0 + 1) by NAT_1: 13;

                  then

                   A85: (i0 - 1) < ((i0 + 1) - 1) by XREAL_1: 14;

                  i0 <= n by A25, A26, FINSEQ_1: 1;

                  then

                   A86: (i0 - 1) < ( len ( Path_matrix (p,( 1. (K,n))))) by A22, A85, XXREAL_0: 2;

                  (i0 -' 1) = (i0 - 1) by A84, XREAL_1: 233;

                  then

                   A87: ((i0 -' 1) + 1) = i0;

                  (i0 - 1) > (1 - 1) by A84, XREAL_1: 14;

                  

                  then (f4 . i0) = (the multF of K . ((f4 . (i0 -' 1)),(( Path_matrix (p,( 1. (K,n)))) . i0))) by A76, A86, A87

                  .= (a * ( 0. K)) by A28, A66, A64, MATRIX_1:def 3

                  .= ( 0. K);

                  hence P5[ 0 ];

                end;

              end;

              then

               A88: P5[ 0 ];

              for k be Nat holds P5[k] from NAT_1:sch 2( A88, A68);

              then P5[(n -' i0)];

              then (f4 . (i0 + (n -' i0))) = ( 0. K);

              hence thesis by A1, A8, A54, A22, A75, A76, A65, FINSOP_1: 2;

            end;

          end;

          hence thesis;

        end;

        hence thesis by MATRIX_3:def 8;

      end;

      deffunc F3( set) = ( IFIN (( idseq n),$1,( 1_ K),( 0. K)));

      set F = the addF of K;

      set f = ( Path_product ( 1. (K,n)));

      set B = ( In (( Permutations n),( Fin ( Permutations n))));

      

       A89: for x be set st x in ( Fin X) holds F3(x) in Y

      proof

        let x be set;

        assume x in ( Fin X);

        now

          per cases ;

            case ( idseq n) in x;

            then F3(x) = ( 1_ K) by Def1;

            hence thesis;

          end;

            case not ( idseq n) in x;

            then F3(x) = ( 0. K) by Def1;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      ex f2 be Function of ( Fin X), Y st for x be set st x in ( Fin X) holds (f2 . x) = F3(x) from FUNCT_2:sch 11( A89);

      then

      consider G0 be Function of ( Fin X), Y such that

       A90: for x be set st x in ( Fin X) holds (G0 . x) = F3(x);

      ( dom f2) = ( Permutations n) by FUNCT_2:def 1;

      then

       A91: ( dom ( Path_product ( 1. (K,n)))) = ( dom f2) by FUNCT_2:def 1;

      then

       A92: ( Path_product ( 1. (K,n))) = f2 by A5, FUNCT_1: 2;

      

       A93: for B9 be Element of ( Fin X) st B9 c= B & B9 <> {} holds for x be Element of X st x in (B \ B9) holds (G0 . (B9 \/ {x})) = (F . ((G0 . B9),(f . x)))

      proof

        let B9 be Element of ( Fin X);

        assume that B9 c= B and B9 <> {} ;

        thus for x be Element of X st x in (B \ B9) holds (G0 . (B9 \/ {x})) = (F . ((G0 . B9),(f . x)))

        proof

          let x be Element of X;

          assume

           A94: x in (B \ B9);

           A95:

          now

            assume

             A96: not ( idseq n) in (B9 \/ {x});

            

            thus (G0 . (B9 \/ {x})) = ( IFIN (( idseq n),(B9 \/ {.x.}),( 1_ K),( 0. K))) by A90

            .= ( 0. K) by A96, Def1;

          end;

          

           A97: ( 0. K) is_a_unity_wrt F by FVSUM_1: 6;

           A98:

          now

            assume

             A99: not ( idseq n) in B9;

            

            thus (G0 . B9) = ( IFIN (( idseq n),B9,( 1_ K),( 0. K))) by A90

            .= ( 0. K) by A99, Def1;

          end;

           A100:

          now

            assume

             A101: not ( idseq n) in (B9 \/ {x});

            then not ( idseq n) in {x} by XBOOLE_0:def 3;

            then

             A102: not ( idseq n) = x by TARSKI:def 1;

            (f . x) = F2(x) by A3, A92

            .= ( 0. K) by A102, FUNCOP_1:def 8;

            hence (F . ((G0 . B9),(f . x))) = ( 0. K) by A98, A97, A101, BINOP_1: 3, XBOOLE_0:def 3;

          end;

           A103:

          now

            assume

             A104: ( idseq n) in B9;

            

            thus (G0 . B9) = ( IFIN (( idseq n),B9,( 1_ K),( 0. K))) by A90

            .= ( 1_ K) by A104, Def1;

          end;

           A105:

          now

            assume ( idseq n) in (B9 \/ {x});

            then

             A106: ( idseq n) in B9 or ( idseq n) in {x} by XBOOLE_0:def 3;

            now

              per cases by A106, TARSKI:def 1;

                case

                 A107: ( idseq n) in B9;

                

                 A108: not x in B9 by A94, XBOOLE_0:def 5;

                (f . x) = F2(x) by A3, A92

                .= ( 0. K) by A107, A108, FUNCOP_1:def 8;

                hence (F . ((G0 . B9),(f . x))) = ( 1_ K) by A103, A97, A107, BINOP_1: 3;

              end;

                case

                 A109: ( idseq n) = x;

                (f . x) = F2(x) by A3, A92

                .= ( 1_ K) by A109, FUNCOP_1:def 8;

                hence (F . ((G0 . B9),(f . x))) = ( 1_ K) by A94, A98, A97, A109, BINOP_1: 3, XBOOLE_0:def 5;

              end;

            end;

            hence (F . ((G0 . B9),(f . x))) = ( 1_ K);

          end;

          now

            assume

             A110: ( idseq n) in (B9 \/ {x});

            

            thus (G0 . (B9 \/ {x})) = ( IFIN (( idseq n),(B9 \/ {.x.}),( 1_ K),( 0. K))) by A90

            .= ( 1_ K) by A110, Def1;

          end;

          hence thesis by A95, A105, A100;

        end;

      end;

      

       A111: for x be Element of X holds (G0 . {x}) = (f . x)

      proof

        let x be Element of X;

        now

          per cases ;

            case

             A112: x = ( idseq n);

            then ( idseq n) in {x} by TARSKI:def 1;

            then

             A113: ( IFIN (( idseq n), {x},( 1_ K),( 0. K))) = ( 1_ K) by Def1;

            (f2 . x) = F2(x) by A3

            .= ( 1_ K) by A112, FUNCOP_1:def 8;

            hence (G0 . {.x.}) = (f2 . x) by A90, A113;

          end;

            case

             A114: x <> ( idseq n);

            then not ( idseq n) in {x} by TARSKI:def 1;

            then

             A115: ( IFIN (( idseq n), {x},( 1_ K),( 0. K))) = ( 0. K) by Def1;

            (f2 . x) = F2(x) by A3

            .= ( 0. K) by A114, FUNCOP_1:def 8;

            hence (G0 . {.x.}) = (f2 . x) by A90, A115;

          end;

        end;

        hence thesis by A91, A5, FUNCT_1: 2;

      end;

      

       A116: for e be Element of Y st e is_a_unity_wrt F holds (G0 . {} ) = e

      proof

        let e be Element of Y;

        assume e is_a_unity_wrt F;

        then

         A117: (F . (( 0. K),e)) = ( 0. K) by BINOP_1: 3;

        ( 0. K) is_a_unity_wrt F by FVSUM_1: 6;

        then

         A118: (F . (( 0. K),e)) = e by BINOP_1: 3;

        ( IFIN (( idseq n), {} ,( 1_ K),( 0. K))) = ( 0. K) by Def1;

        hence thesis by A90, A117, A118, FINSUB_1: 7;

      end;

       A119:

      now

        assume

         A120: ( idseq n) in B;

        

        thus (G0 . B) = ( IFIN (( idseq n),B,( 1_ K),( 0. K))) by A90

        .= ( 1_ K) by A120, Def1;

      end;

      

       S: ( idseq n) is Element of ( Group_of_Perm n) by MATRIX_1: 11;

      ( Permutations n) in ( Fin ( Permutations n)) by FINSUB_1:def 5;

      then B = ( Permutations n) & ( idseq n) in the carrier of ( Group_of_Perm n) by S, SUBSET_1:def 8;

      then (the addF of K $$ (( In (( Permutations n),( Fin ( Permutations n)))),( Path_product ( 1. (K,n))))) = ( 1_ K) by A119, A116, A111, A93, MATRIX_1:def 13, SETWISEO:def 3;

      hence thesis by MATRIX_3:def 9;

    end;

    definition

      let n be Nat, K be Field, M be Matrix of n, K;

      :: original: diagonal

      redefine

      :: MATRIX_7:def2

      attr M is diagonal means for i,j be Nat st i in ( Seg n) & j in ( Seg n) & i <> j holds (M * (i,j)) = ( 0. K);

      compatibility

      proof

        hereby

          assume

           A1: M is diagonal;

          let i,j be Nat;

          assume that

           A2: i in ( Seg n) & j in ( Seg n) and

           A3: i <> j;

           [i, j] in [:( Seg n), ( Seg n):] by A2, ZFMISC_1:def 2;

          then [i, j] in ( Indices M) by MATRIX_0: 24;

          hence (M * (i,j)) = ( 0. K) by A1, A3;

        end;

        assume

         A4: for i,j be Nat st i in ( Seg n) & j in ( Seg n) & i <> j holds (M * (i,j)) = ( 0. K);

        let i,j be Nat;

        assume that

         A5: [i, j] in ( Indices M) and

         A6: (M * (i,j)) <> ( 0. K);

         [i, j] in [:( Seg n), ( Seg n):] by A5, MATRIX_0: 24;

        then i in ( Seg n) & j in ( Seg n) by ZFMISC_1: 87;

        hence thesis by A4, A6;

      end;

    end

    theorem :: MATRIX_7:17

    for K be Field, n be Nat, A be Matrix of n, K st n >= 1 & A is diagonal holds ( Det A) = (the multF of K $$ ( diagonal_of_Matrix A))

    proof

      let K be Field, n be Nat, A be Matrix of n, K;

      assume that

       A1: n >= 1 and

       A2: A is diagonal;

      set k1 = (the multF of K $$ ( diagonal_of_Matrix A));

      set X = ( Permutations n);

      set Y = the carrier of K;

      reconsider p0 = ( idseq n) as Permutation of ( Seg n);

      

       A3: ( len ( diagonal_of_Matrix A)) = n by MATRIX_3:def 10;

      deffunc F2( object) = ( IFEQ (( idseq n),$1,k1,( 0. K)));

      

       A4: for x be object st x in X holds F2(x) in Y;

      ex f2 be Function of X, Y st for x be object st x in X holds (f2 . x) = F2(x) from FUNCT_2:sch 2( A4);

      then

      consider f2 be Function of X, Y such that

       A5: for x be object st x in X holds (f2 . x) = F2(x);

      

       A6: p0 is even by MATRIX_1: 16;

      

       A7: for x be object st x in ( dom ( Path_product A)) holds (( Path_product A) . x) = (f2 . x)

      proof

        let x be object;

        assume x in ( dom ( Path_product A));

        for p be Element of ( Permutations n) holds (f2 . p) = ( - ((the multF of K $$ ( Path_matrix (p,A))),p))

        proof

          let p be Element of ( Permutations n);

           A8:

          now

            per cases ;

              suppose p is even;

              hence ( - (( 0. K),p)) = ( 0. K) by MATRIX_1:def 16;

            end;

              suppose p is odd;

              

              then ( - (( 0. K),p)) = ( - ( 0. K)) by MATRIX_1:def 16

              .= ( 0. K) by RLVECT_1: 12;

              hence ( - (( 0. K),p)) = ( 0. K);

            end;

          end;

          now

            per cases ;

              case

               A9: p = ( idseq n);

              

               A10: for i, j st i in ( dom ( diagonal_of_Matrix A)) & j = (p . i) holds (( diagonal_of_Matrix A) . i) = (A * (i,j))

              proof

                let i, j;

                assume that

                 A11: i in ( dom ( diagonal_of_Matrix A)) and

                 A12: j = (p . i);

                

                 A13: i in ( Seg n) by A3, A11, FINSEQ_1:def 3;

                then (p . i) = i by A9, FUNCT_1: 17;

                hence thesis by A12, A13, MATRIX_3:def 10;

              end;

              ( len ( Permutations n)) = n by MATRIX_1: 9;

              then

               A14: ( - ((the multF of K $$ ( Path_matrix (p,A))),p)) = (the multF of K $$ ( Path_matrix (p,A))) by A6, A9, MATRIX_1:def 16;

              (f2 . p) = F2(p) by A5

              .= k1 by A9, FUNCOP_1:def 8;

              hence thesis by A3, A14, A10, MATRIX_3:def 7;

            end;

              case

               A15: p <> ( idseq n);

              reconsider Ab = NAT as non empty set;

              defpred P3[ Nat] means $1 < n implies ex p3 be FinSequence of K st ( len p3) = ($1 + 1) & (p3 . 1) = (( Path_matrix (p,A)) . 1) & (for n3 be Nat st 0 <> n3 & n3 < ($1 + 1) & n3 < n holds (p3 . (n3 + 1)) = (the multF of K . ((p3 . n3),(( Path_matrix (p,A)) . (n3 + 1)))));

              

               A16: ( rng ( Path_matrix (p,A))) c= the carrier of K by FINSEQ_1:def 4;

              

               A17: ( len ( Path_matrix (p,A))) = n by MATRIX_3:def 7;

              then 1 in ( Seg ( len ( Path_matrix (p,A)))) by A1;

              then 1 in ( dom ( Path_matrix (p,A))) by FINSEQ_1:def 3;

              then (( Path_matrix (p,A)) . 1) in ( rng ( Path_matrix (p,A))) by FUNCT_1:def 3;

              then

              reconsider d = (( Path_matrix (p,A)) . 1) as Element of K by A16;

              reconsider q3 = <*d*> as FinSequence of K;

              

               A18: for n3 be Nat st 0 <> n3 & n3 < ( 0 + 1) & n3 < n holds (q3 . (n3 + 1)) = (the multF of K . ((q3 . n3),(( Path_matrix (p,A)) . (n3 + 1)))) by NAT_1: 13;

              

               A19: for k be Nat st P3[k] holds P3[(k + 1)]

              proof

                let k be Nat;

                assume

                 A20: P3[k];

                now

                  per cases ;

                    case

                     A21: (k + 1) < n;

                    then

                    consider p3 be FinSequence of K such that

                     A22: ( len p3) = (k + 1) and

                     A23: (p3 . 1) = (( Path_matrix (p,A)) . 1) and

                     A24: for n3 be Nat st 0 <> n3 & n3 < (k + 1) & n3 < n holds (p3 . (n3 + 1)) = (the multF of K . ((p3 . n3),(( Path_matrix (p,A)) . (n3 + 1)))) by A20, NAT_1: 12;

                    defpred P6[ object, object] means ($1 in ( Seg (k + 1)) implies $2 = (p3 . $1)) & ( not $1 in ( Seg (k + 1)) implies $2 = ( 0. K));

                    

                     A25: for x be object st x in NAT holds ex y be object st y in the carrier of K & P6[x, y]

                    proof

                      let x be object;

                      assume x in NAT ;

                      now

                        per cases ;

                          case

                           A26: x in ( Seg (k + 1));

                          then

                          reconsider nx = x as Nat;

                          nx in ( dom p3) by A22, A26, FINSEQ_1:def 3;

                          then

                           A27: (p3 . nx) in ( rng p3) by FUNCT_1:def 3;

                          ( rng p3) c= the carrier of K by FINSEQ_1:def 4;

                          then

                          reconsider s = (p3 . nx) as Element of K by A27;

                          x in ( Seg (k + 1)) implies s = (p3 . x);

                          hence thesis by A26;

                        end;

                          case not x in ( Seg (k + 1));

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                    ex f6 be sequence of the carrier of K st for x be object st x in NAT holds P6[x, (f6 . x)] from FUNCT_2:sch 1( A25);

                    then

                    consider f6 be sequence of the carrier of K such that

                     A28: for x be object st x in NAT holds P6[x, (f6 . x)];

                    1 <= ((k + 1) + 1) & ((k + 1) + 1) <= n by A21, NAT_1: 12, NAT_1: 13;

                    then ((k + 1) + 1) in ( Seg ( len ( Path_matrix (p,A)))) by A17;

                    then ((k + 1) + 1) in ( dom ( Path_matrix (p,A))) by FINSEQ_1:def 3;

                    then ( rng ( Path_matrix (p,A))) c= the carrier of K & (( Path_matrix (p,A)) . ((k + 1) + 1)) in ( rng ( Path_matrix (p,A))) by FINSEQ_1:def 4, FUNCT_1:def 3;

                    then [(f6 . (k + 1)), (( Path_matrix (p,A)) . ((k + 1) + 1))] in [:the carrier of K, the carrier of K:] by ZFMISC_1:def 2;

                    then

                    reconsider e = (the multF of K . ((f6 . (k + 1)),(( Path_matrix (p,A)) . ((k + 1) + 1)))) as Element of K by FUNCT_2: 5;

                    reconsider q3 = (p3 ^ <*e*>) as FinSequence of K;

                    

                     A29: ( len q3) = (( len p3) + ( len <*e*>)) by FINSEQ_1: 22

                    .= ((k + 1) + 1) by A22, FINSEQ_1: 40;

                    

                     A30: for n3 be Nat st 0 <> n3 & n3 < ((k + 1) + 1) & n3 < n holds (q3 . (n3 + 1)) = (the multF of K . ((q3 . n3),(( Path_matrix (p,A)) . (n3 + 1))))

                    proof

                      let n3 be Nat;

                      assume that

                       A31: 0 <> n3 and

                       A32: n3 < ((k + 1) + 1) and

                       A33: n3 < n;

                      now

                        per cases ;

                          case

                           A34: n3 < (k + 1);

                          then 1 <= (n3 + 1) & (n3 + 1) <= (k + 1) by NAT_1: 12, NAT_1: 13;

                          then (n3 + 1) in ( Seg ( len p3)) by A22;

                          then (n3 + 1) in ( dom p3) by FINSEQ_1:def 3;

                          then

                           A35: (p3 . (n3 + 1)) = (q3 . (n3 + 1)) by FINSEQ_1:def 7;

                          ( 0 + 1) <= n3 by A31, NAT_1: 13;

                          then n3 in ( Seg ( len p3)) by A22, A34;

                          then

                           A36: n3 in ( dom p3) by FINSEQ_1:def 3;

                          (p3 . (n3 + 1)) = (the multF of K . ((p3 . n3),(( Path_matrix (p,A)) . (n3 + 1)))) by A24, A31, A33, A34;

                          hence thesis by A35, A36, FINSEQ_1:def 7;

                        end;

                          case

                           A37: n3 >= (k + 1);

                          

                           A38: (n3 + 1) <= ((k + 1) + 1) by A32, NAT_1: 13;

                          

                           A39: (n3 + 1) > (k + 1) by A37, NAT_1: 13;

                          then (n3 + 1) >= ((k + 1) + 1) by NAT_1: 13;

                          then

                           A40: (n3 + 1) = ((k + 1) + 1) by A38, XXREAL_0: 1;

                          1 <= (k + 1) by NAT_1: 12;

                          then

                           A41: (k + 1) in ( Seg (k + 1));

                          then (k + 1) in ( dom p3) by A22, FINSEQ_1:def 3;

                          then

                           A42: (q3 . (k + 1)) = (p3 . (k + 1)) by FINSEQ_1:def 7;

                          (q3 . (n3 + 1)) = ( <*e*> . ((n3 + 1) - (k + 1))) by A22, A29, A39, A38, FINSEQ_1: 24

                          .= e by A40, FINSEQ_1:def 8;

                          hence thesis by A28, A40, A41, A42;

                        end;

                      end;

                      hence thesis;

                    end;

                    1 <= (k + 1) by NAT_1: 12;

                    then 1 in ( Seg ( len p3)) by A22;

                    then 1 in ( dom p3) by FINSEQ_1:def 3;

                    then (q3 . 1) = (( Path_matrix (p,A)) . 1) by A23, FINSEQ_1:def 7;

                    hence thesis by A29, A30;

                  end;

                    case (k + 1) >= n;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

              

               A43: (f2 . p) = F2(p) by A5

              .= ( 0. K) by A15, FUNCOP_1:def 8;

              n < (n + 1) by NAT_1: 13;

              then

               A44: (n - 1) < ((n + 1) - 1) by XREAL_1: 14;

              

               A45: ( dom p) = ( Seg ( len ( Permutations n))) by FUNCT_2: 52;

              then

               A46: ( dom p) = ( Seg n) by MATRIX_1: 9;

              then ( dom p) = ( dom ( idseq n)) by RELAT_1: 45;

              then

              consider i0 be object such that

               A47: i0 in ( dom p) and

               A48: (p . i0) <> (( idseq n) . i0) by A15, FUNCT_1: 2;

              

               A49: i0 in ( Seg n) by A45, A47, MATRIX_1: 9;

              reconsider i0 as Nat by A45, A47;

              

               A50: (p . i0) <> i0 by A46, A47, A48, FUNCT_1: 18;

              p is Permutation of ( Seg n) by MATRIX_1:def 12;

              then

               A51: (p . i0) in ( Seg n) by A46, A47, FUNCT_2: 5;

              then

              reconsider j0 = (p . i0) as Nat;

              

               A52: (n - 1) = (n -' 1) by A1, XREAL_1: 233;

              ( len q3) = 1 & (q3 . 1) = (( Path_matrix (p,A)) . 1) by FINSEQ_1: 40;

              then

               A53: P3[ 0 ] by A18;

              for k be Nat holds P3[k] from NAT_1:sch 2( A53, A19);

              then

              consider p3 be FinSequence of K such that

               A54: ( len p3) = ((n -' 1) + 1) and

               A55: (p3 . 1) = (( Path_matrix (p,A)) . 1) and

               A56: for n3 be Nat st 0 <> n3 & n3 < ((n -' 1) + 1) & n3 < n holds (p3 . (n3 + 1)) = (the multF of K . ((p3 . n3),(( Path_matrix (p,A)) . (n3 + 1)))) by A52, A44;

              defpred P[ set, set] means ($1 in ( Seg n) implies $2 = (p3 . $1)) & ( not $1 in ( Seg n) implies $2 = ( 0. K));

              

               A57: for x3 be Element of Ab holds ex y3 be Element of K st P[x3, y3]

              proof

                let x3 be Element of Ab;

                now

                  per cases ;

                    case

                     A58: x3 in ( Seg n);

                    then x3 in ( dom p3) by A52, A54, FINSEQ_1:def 3;

                    then ( rng p3) c= the carrier of K & (p3 . x3) in ( rng p3) by FINSEQ_1:def 4, FUNCT_1:def 3;

                    hence thesis by A58;

                  end;

                    case not x3 in ( Seg n);

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

              ex f4 be Function of Ab, the carrier of K st for x2 be Element of Ab holds P[x2, (f4 . x2)] from FUNCT_2:sch 3( A57);

              then

              consider f4 be sequence of the carrier of K such that

               A59: for x4 be Element of NAT holds (x4 in ( Seg n) implies (f4 . x4) = (p3 . x4)) & ( not x4 in ( Seg n) implies (f4 . x4) = ( 0. K));

              

               A60: for n3 be Nat st 0 <> n3 & n3 < ( len ( Path_matrix (p,A))) holds (f4 . (n3 + 1)) = (the multF of K . ((f4 . n3),(( Path_matrix (p,A)) . (n3 + 1))))

              proof

                let n3 be Nat;

                assume that

                 A61: 0 <> n3 and

                 A62: n3 < ( len ( Path_matrix (p,A)));

                

                 A63: (n3 + 1) <= ( len ( Path_matrix (p,A))) by A62, NAT_1: 13;

                

                 A64: ( 0 + 1) <= n3 by A61, NAT_1: 13;

                then

                 A65: n3 in ( Seg n) by A17, A62;

                1 < (n3 + 1) by A64, NAT_1: 13;

                then (n3 + 1) in ( Seg n) by A17, A63;

                then

                 A66: (f4 . (n3 + 1)) = (p3 . (n3 + 1)) by A59;

                (p3 . (n3 + 1)) = (the multF of K . ((p3 . n3),(( Path_matrix (p,A)) . (n3 + 1)))) by A17, A52, A56, A61, A62;

                hence thesis by A59, A66, A65;

              end;

              

               A67: i0 <= n by A46, A47, FINSEQ_1: 1;

              then

               A68: (n -' i0) = (n - i0) by XREAL_1: 233;

              i0 in ( dom ( Path_matrix (p,A))) by A49, A17, FINSEQ_1:def 3;

              then

               A69: (( Path_matrix (p,A)) . i0) = (A * (i0,j0)) by MATRIX_3:def 7;

              defpred P5[ Nat] means (f4 . (i0 + $1)) = ( 0. K);

              

               A70: 0 < i0 by A45, A47, FINSEQ_1: 1;

              

               A71: for k be Nat st P5[k] holds P5[(k + 1)]

              proof

                let k be Nat;

                

                 A72: 1 <= (1 + (i0 + k)) by NAT_1: 12;

                assume

                 A73: P5[k];

                now

                  per cases ;

                    case

                     A74: ((i0 + k) + 1) <= n;

                    1 <= (1 + (i0 + k)) by NAT_1: 12;

                    then ((i0 + k) + 1) in ( Seg ( len ( Path_matrix (p,A)))) by A17, A74;

                    then ((i0 + k) + 1) in ( dom ( Path_matrix (p,A))) by FINSEQ_1:def 3;

                    then

                     A75: (( Path_matrix (p,A)) . ((i0 + k) + 1)) in ( rng ( Path_matrix (p,A))) by FUNCT_1:def 3;

                    ( rng ( Path_matrix (p,A))) c= the carrier of K by FINSEQ_1:def 4;

                    then

                    reconsider b = (( Path_matrix (p,A)) . ((i0 + k) + 1)) as Element of K by A75;

                    i0 <= (i0 + k) by NAT_1: 12;

                    then

                     A76: 0 < (i0 + k) by A45, A47, FINSEQ_1: 1;

                    

                     A77: (i0 + k) < n by A74, NAT_1: 13;

                    ( 0 + 1) <= (i0 + k) by A70, NAT_1: 13;

                    then

                     A78: (i0 + k) in ( Seg n) by A77;

                    ((i0 + k) + 1) in ( Seg n) by A72, A74;

                    

                    then (f4 . ((i0 + k) + 1)) = (p3 . ((i0 + k) + 1)) by A59

                    .= (the multF of K . ((p3 . (i0 + k)),(( Path_matrix (p,A)) . ((i0 + k) + 1)))) by A52, A56, A77, A76

                    .= (( 0. K) * b) by A59, A73, A78

                    .= ( 0. K);

                    hence thesis;

                  end;

                    case ((i0 + k) + 1) > n;

                    then not (i0 + (k + 1)) in ( Seg n) by FINSEQ_1: 1;

                    hence thesis by A59;

                  end;

                end;

                hence thesis;

              end;

              1 in ( Seg n) by A1;

              then

               A79: (f4 . 1) = (( Path_matrix (p,A)) . 1) by A55, A59;

              

               A80: 1 <= i0 by A45, A47, FINSEQ_1: 1;

              now

                per cases ;

                  case i0 <= 1;

                  then i0 = 1 by A80, XXREAL_0: 1;

                  hence P5[ 0 ] by A2, A49, A50, A51, A69, A79;

                end;

                  case

                   A81: i0 > 1;

                  reconsider a = (f4 . (i0 -' 1)) as Element of K;

                  i0 < (i0 + 1) by NAT_1: 13;

                  then (i0 - 1) < ((i0 + 1) - 1) by XREAL_1: 14;

                  then

                   A82: (i0 - 1) < ( len ( Path_matrix (p,A))) by A67, A17, XXREAL_0: 2;

                  (i0 -' 1) = (i0 - 1) by A81, XREAL_1: 233;

                  then

                   A83: ((i0 -' 1) + 1) = i0;

                  (i0 - 1) > (1 - 1) by A81, XREAL_1: 14;

                  

                  then (f4 . i0) = (the multF of K . ((f4 . (i0 -' 1)),(( Path_matrix (p,A)) . i0))) by A60, A82, A83

                  .= (a * ( 0. K)) by A2, A49, A50, A51, A69

                  .= ( 0. K);

                  hence P5[ 0 ];

                end;

              end;

              then

               A84: P5[ 0 ];

              for k be Nat holds P5[k] from NAT_1:sch 2( A84, A71);

              then P5[(n -' i0)];

              hence thesis by A1, A8, A43, A17, A79, A60, A68, FINSOP_1: 2;

            end;

          end;

          hence thesis;

        end;

        hence thesis by MATRIX_3:def 8;

      end;

      deffunc F3( set) = ( IFIN (( idseq n),$1,k1,( 0. K)));

      set F = the addF of K;

      set f = ( Path_product A);

      set B = ( In (( Permutations n),( Fin ( Permutations n))));

      

       A85: for x be set st x in ( Fin X) holds F3(x) in Y

      proof

        let x be set;

        assume x in ( Fin X);

        per cases ;

          suppose ( idseq n) in x;

          then F3(x) = k1 by Def1;

          hence thesis;

        end;

          suppose not ( idseq n) in x;

          then F3(x) = ( 0. K) by Def1;

          hence thesis;

        end;

      end;

      ex f2 be Function of ( Fin X), Y st for x be set st x in ( Fin X) holds (f2 . x) = F3(x) from FUNCT_2:sch 11( A85);

      then

      consider G0 be Function of ( Fin X), Y such that

       A86: for x be set st x in ( Fin X) holds (G0 . x) = F3(x);

      ( dom f2) = ( Permutations n) by FUNCT_2:def 1;

      then

       A87: ( dom ( Path_product A)) = ( dom f2) by FUNCT_2:def 1;

      then

       A88: ( Path_product A) = f2 by A7, FUNCT_1: 2;

      

       A89: for B9 be Element of ( Fin X) st B9 c= B & B9 <> {} holds for x be Element of X st x in (B \ B9) holds (G0 . (B9 \/ {x})) = (F . ((G0 . B9),(f . x)))

      proof

        let B9 be Element of ( Fin X);

        assume that B9 c= B and B9 <> {} ;

        thus for x be Element of X st x in (B \ B9) holds (G0 . (B9 \/ {x})) = (F . ((G0 . B9),(f . x)))

        proof

          let x be Element of X;

          assume

           A90: x in (B \ B9);

           A91:

          now

            assume

             A92: not ( idseq n) in (B9 \/ {x});

            

            thus (G0 . (B9 \/ {x})) = ( IFIN (( idseq n),(B9 \/ {.x.}),k1,( 0. K))) by A86

            .= ( 0. K) by A92, Def1;

          end;

          

           A93: ( 0. K) is_a_unity_wrt F by FVSUM_1: 6;

           A94:

          now

            assume

             A95: not ( idseq n) in B9;

            

            thus (G0 . B9) = ( IFIN (( idseq n),B9,k1,( 0. K))) by A86

            .= ( 0. K) by A95, Def1;

          end;

           A96:

          now

            assume

             A97: not ( idseq n) in (B9 \/ {x});

            then not ( idseq n) in {x} by XBOOLE_0:def 3;

            then

             A98: not ( idseq n) = x by TARSKI:def 1;

            (f . x) = F2(x) by A5, A88

            .= ( 0. K) by A98, FUNCOP_1:def 8;

            hence (F . ((G0 . B9),(f . x))) = ( 0. K) by A94, A93, A97, BINOP_1: 3, XBOOLE_0:def 3;

          end;

           A99:

          now

            assume

             A100: ( idseq n) in B9;

            

            thus (G0 . B9) = ( IFIN (( idseq n),B9,k1,( 0. K))) by A86

            .= k1 by A100, Def1;

          end;

           A101:

          now

            assume ( idseq n) in (B9 \/ {x});

            then

             A102: ( idseq n) in B9 or ( idseq n) in {x} by XBOOLE_0:def 3;

            now

              per cases by A102, TARSKI:def 1;

                case

                 A103: ( idseq n) in B9;

                

                 A104: not x in B9 by A90, XBOOLE_0:def 5;

                (f . x) = F2(x) by A5, A88

                .= ( 0. K) by A103, A104, FUNCOP_1:def 8;

                hence (F . ((G0 . B9),(f . x))) = k1 by A99, A93, A103, BINOP_1: 3;

              end;

                case

                 A105: ( idseq n) = x;

                (f . x) = F2(x) by A5, A88

                .= k1 by A105, FUNCOP_1:def 8;

                hence (F . ((G0 . B9),(f . x))) = k1 by A90, A94, A93, A105, BINOP_1: 3, XBOOLE_0:def 5;

              end;

            end;

            hence (F . ((G0 . B9),(f . x))) = k1;

          end;

          now

            assume

             A106: ( idseq n) in (B9 \/ {x});

            

            thus (G0 . (B9 \/ {x})) = ( IFIN (( idseq n),(B9 \/ {.x.}),k1,( 0. K))) by A86

            .= k1 by A106, Def1;

          end;

          hence thesis by A91, A101, A96;

        end;

      end;

      

       A107: for x be Element of X holds (G0 . {x}) = (f . x)

      proof

        let x be Element of X;

        now

          per cases ;

            case

             A108: x = ( idseq n);

            then ( idseq n) in {x} by TARSKI:def 1;

            then

             A109: ( IFIN (( idseq n), {x},k1,( 0. K))) = k1 by Def1;

            (f2 . x) = F2(x) by A5

            .= k1 by A108, FUNCOP_1:def 8;

            hence (G0 . {.x.}) = (f2 . x) by A86, A109;

          end;

            case

             A110: x <> ( idseq n);

            then not ( idseq n) in {x} by TARSKI:def 1;

            then

             A111: ( IFIN (( idseq n), {x},k1,( 0. K))) = ( 0. K) by Def1;

            (f2 . x) = F2(x) by A5

            .= ( 0. K) by A110, FUNCOP_1:def 8;

            hence (G0 . {.x.}) = (f2 . x) by A86, A111;

          end;

        end;

        hence thesis by A87, A7, FUNCT_1: 2;

      end;

      

       A112: for e be Element of Y st e is_a_unity_wrt F holds (G0 . {} ) = e

      proof

        let e be Element of Y;

        assume e is_a_unity_wrt F;

        then

         A113: (F . (( 0. K),e)) = ( 0. K) by BINOP_1: 3;

        ( 0. K) is_a_unity_wrt F by FVSUM_1: 6;

        then

         A114: (F . (( 0. K),e)) = e by BINOP_1: 3;

        ( IFIN (( idseq n), {} ,k1,( 0. K))) = ( 0. K) by Def1;

        hence thesis by A86, A113, A114, FINSUB_1: 7;

      end;

       A115:

      now

        assume

         A116: ( idseq n) in B;

        

        thus (G0 . B) = ( IFIN (( idseq n),B,k1,( 0. K))) by A86

        .= (the multF of K $$ ( diagonal_of_Matrix A)) by A116, Def1;

      end;

      

       S: ( idseq n) is Element of ( Group_of_Perm n) by MATRIX_1: 11;

      ( Permutations n) in ( Fin ( Permutations n)) by FINSUB_1:def 5;

      then B = ( Permutations n) & ( idseq n) in the carrier of ( Group_of_Perm n) by S, SUBSET_1:def 8;

      then (the addF of K $$ (( In (( Permutations n),( Fin ( Permutations n)))),( Path_product A))) = (the multF of K $$ ( diagonal_of_Matrix A)) by A115, A112, A107, A89, MATRIX_1:def 13, SETWISEO:def 3;

      hence thesis by MATRIX_3:def 9;

    end;

    theorem :: MATRIX_7:18

    

     Th18: for p be Element of ( Permutations n) holds (p " ) is Element of ( Permutations n)

    proof

      let p be Element of ( Permutations n);

      (p " ) is Element of ( Group_of_Perm n) by MATRIX_1: 14;

      hence thesis by MATRIX_1:def 13;

    end;

    definition

      let n;

      let p be Element of ( Permutations n);

      :: original: "

      redefine

      func p " -> Element of ( Permutations n) ;

      coherence by Th18;

    end

    ::$Canceled

    theorem :: MATRIX_7:20

    for G be Group, f1,f2 be FinSequence of G holds (( Product (f1 ^ f2)) " ) = ((( Product f2) " ) * (( Product f1) " ))

    proof

      let G be Group, f1,f2 be FinSequence of G;

      

      thus (( Product (f1 ^ f2)) " ) = ((( Product f1) * ( Product f2)) " ) by GROUP_4: 5

      .= ((( Product f2) " ) * (( Product f1) " )) by GROUP_1: 17;

    end;

    definition

      let G be Group, f be FinSequence of G;

      ::$Canceled

      :: MATRIX_7:def4

      func f " -> FinSequence of G means

      : Def3: ( len it ) = ( len f) & for i be Nat st i in ( dom f) holds (it /. i) = ((f /. i) " );

      existence

      proof

        deffunc F( Nat) = ((f /. $1) " );

        ex p be FinSequence st ( len p) = ( len f) & for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;

        then

        consider p be FinSequence such that

         A1: ( len p) = ( len f) and

         A2: for k be Nat st k in ( dom p) holds (p . k) = F(k);

        ( rng p) c= the carrier of G

        proof

          let y be object;

          assume y in ( rng p);

          then

          consider x be object such that

           A3: x in ( dom p) and

           A4: y = (p . x) by FUNCT_1:def 3;

          reconsider k = x as Nat by A3;

          (p . k) = ((f /. k) " ) by A2, A3;

          hence thesis by A4;

        end;

        then

        reconsider q = p as FinSequence of G by FINSEQ_1:def 4;

        

         A5: ( dom p) = ( dom f) by A1, FINSEQ_3: 29;

        for i be Nat st i in ( dom f) holds (q /. i) = ((f /. i) " )

        proof

          let i be Nat;

          assume

           A6: i in ( dom f);

          

          hence (q /. i) = (p . i) by A5, PARTFUN1:def 6

          .= ((f /. i) " ) by A2, A5, A6;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        thus for g1,g2 be FinSequence of G st (( len g1) = ( len f) & for i be Nat st i in ( dom f) holds (g1 /. i) = ((f /. i) " )) & (( len g2) = ( len f) & for j be Nat st j in ( dom f) holds (g2 /. j) = ((f /. j) " )) holds g1 = g2

        proof

          let g1,g2 be FinSequence of G;

          assume that

           A7: ( len g1) = ( len f) and

           A8: for i be Nat st i in ( dom f) holds (g1 /. i) = ((f /. i) " ) and

           A9: ( len g2) = ( len f) and

           A10: for j be Nat st j in ( dom f) holds (g2 /. j) = ((f /. j) " );

          

           A11: ( dom g1) = ( dom f) by A7, FINSEQ_3: 29;

          for k be Nat st 1 <= k & k <= ( len g1) holds (g1 . k) = (g2 . k)

          proof

            let k be Nat;

            assume

             A12: 1 <= k & k <= ( len g1);

            k in ( Seg ( len g2)) by A7, A9, A12;

            then k in ( dom g2) by FINSEQ_1:def 3;

            then

             A13: (g2 . k) = (g2 /. k) by PARTFUN1:def 6;

            k in ( Seg ( len g1)) by A12;

            then

             A14: k in ( dom g1) by FINSEQ_1:def 3;

            then (g1 . k) = (g1 /. k) & (g1 /. k) = ((f /. k) " ) by A8, A11, PARTFUN1:def 6;

            hence thesis by A10, A11, A14, A13;

          end;

          hence thesis by A7, A9;

        end;

      end;

    end

    theorem :: MATRIX_7:21

    

     Th20: for G be Group holds (( <*> the carrier of G) " ) = ( <*> the carrier of G)

    proof

      let G be Group;

      ( len ( <*> the carrier of G)) = 0 ;

      then ( len (( <*> the carrier of G) " ) qua FinSequence of G) = 0 by Def3;

      hence thesis;

    end;

    theorem :: MATRIX_7:22

    

     Th21: for G be Group, f,g be FinSequence of G holds ((f ^ g) " ) = ((f " ) ^ (g " ))

    proof

      let G be Group, f,g be FinSequence of G;

      

       A1: ( len ((f ^ g) " )) = ( len (f ^ g)) by Def3

      .= (( len f) + ( len g)) by FINSEQ_1: 22;

      

       A2: (( len f) + ( len g)) = (( len (f " )) + ( len g)) by Def3

      .= (( len (f " )) + ( len (g " ))) by Def3

      .= ( len ((f " ) ^ (g " ))) by FINSEQ_1: 22;

      

       A3: ( len ((f ^ g) " )) = ( len (f ^ g)) by Def3;

      for i be Nat st 1 <= i & i <= ( len ((f ^ g) " )) holds (((f ^ g) " ) . i) = (((f " ) ^ (g " )) . i)

      proof

        let i be Nat;

        assume that

         A4: 1 <= i and

         A5: i <= ( len ((f ^ g) " ));

        now

          per cases ;

            case ( len f) > 0 ;

            

             A6: ( len (f " )) = ( len f) by Def3;

            ( len ((f ^ g) " )) = ( len (f ^ g)) by Def3;

            then

             A7: ( dom ((f ^ g) " )) = ( dom (f ^ g)) by FINSEQ_3: 29;

            i in ( Seg ( len ((f ^ g) " ))) by A4, A5;

            then

             A8: i in ( dom ((f ^ g) " )) by FINSEQ_1:def 3;

            

            then

             A9: (((f ^ g) " ) . i) = (((f ^ g) " ) /. i) by PARTFUN1:def 6

            .= (((f ^ g) /. i) " ) by A7, A8, Def3;

            

             A10: ( len (g " )) = ( len g) by Def3;

            now

              per cases ;

                case i <= ( len f);

                then

                 A11: i in ( Seg ( len f)) by A4;

                then

                 A12: i in ( dom f) by FINSEQ_1:def 3;

                

                 A13: i in ( dom (f " )) by A6, A11, FINSEQ_1:def 3;

                ((f ^ g) /. i) = ((f ^ g) . i) by A7, A8, PARTFUN1:def 6

                .= (f . i) by A12, FINSEQ_1:def 7

                .= (f /. i) by A12, PARTFUN1:def 6;

                

                then (((f ^ g) /. i) " ) = ((f " ) /. i) by A12, Def3

                .= ((f " ) . i) by A13, PARTFUN1:def 6;

                hence thesis by A9, A13, FINSEQ_1:def 7;

              end;

                case

                 A14: i > ( len f);

                then (1 + ( len f)) <= i by NAT_1: 13;

                then

                 A15: ((1 + ( len f)) - ( len f)) <= (i - ( len f)) by XREAL_1: 9;

                

                 A16: (i -' ( len f)) = (i - ( len f)) by A14, XREAL_1: 233;

                (i - ( len f)) <= ((( len g) + ( len f)) - ( len f)) by A1, A5, XREAL_1: 9;

                then

                 A17: (i -' ( len f)) in ( Seg ( len g)) by A16, A15;

                then

                 A18: (i -' ( len f)) in ( dom g) by FINSEQ_1:def 3;

                

                 A19: (i -' ( len f)) in ( dom (g " )) by A10, A17, FINSEQ_1:def 3;

                ((f ^ g) /. i) = ((f ^ g) . i) by A7, A8, PARTFUN1:def 6

                .= (g . (i - ( len f))) by A3, A5, A14, FINSEQ_1: 24

                .= (g /. (i -' ( len f))) by A16, A18, PARTFUN1:def 6;

                

                then (((f ^ g) /. i) " ) = ((g " ) /. (i -' ( len f))) by A18, Def3

                .= ((g " ) . (i - ( len (f " )))) by A6, A16, A19, PARTFUN1:def 6;

                hence thesis by A1, A2, A5, A6, A9, A14, FINSEQ_1: 24;

              end;

            end;

            hence thesis;

          end;

            case ( len f) <= 0 ;

            then f = {} ;

            then ((f ^ g) " ) = (g " ) & (f " ) = ( <*> the carrier of G) by Th20, FINSEQ_1: 34;

            hence thesis by FINSEQ_1: 34;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A1, A2;

    end;

    theorem :: MATRIX_7:23

    

     Th22: for G be Group, a be Element of G holds ( <*a*> " ) = <*(a " )*>

    proof

      let G be Group, a be Element of G;

      

       A1: ( len ( <*a*> " )) = ( len <*a*>) by Def3

      .= 1 by FINSEQ_1: 39

      .= ( len <*(a " )*>) by FINSEQ_1: 39;

      for i be Nat st 1 <= i & i <= ( len <*(a " )*>) holds (( <*a*> " ) . i) = ( <*(a " )*> . i)

      proof

        let i be Nat;

        assume

         A2: 1 <= i & i <= ( len <*(a " )*>);

        

         A3: ( len <*(a " )*>) = 1 by FINSEQ_1: 39;

        then

         A4: i = 1 by A2, XXREAL_0: 1;

        ( len <*a*>) = 1 by FINSEQ_1: 39;

        then i in ( Seg ( len <*a*>)) by A2, A3;

        then

         A5: i in ( dom <*a*>) by FINSEQ_1:def 3;

        i in ( Seg ( len ( <*a*> " ))) by A1, A2;

        then i in ( dom ( <*a*> " )) by FINSEQ_1:def 3;

        

        then

         A6: (( <*a*> " ) . i) = (( <*a*> " ) /. i) by PARTFUN1:def 6

        .= (( <*a*> /. i) " ) by A5, Def3;

        ( <*a*> /. i) = ( <*a*> . i) by A5, PARTFUN1:def 6

        .= a by A4, FINSEQ_1: 40;

        hence thesis by A4, A6, FINSEQ_1: 40;

      end;

      hence thesis by A1;

    end;

    theorem :: MATRIX_7:24

    

     Th23: for G be Group, f be FinSequence of G holds ( Product (f ^ (( Rev f) " ))) = ( 1_ G)

    proof

      let G be Group, f be FinSequence of G;

      defpred P[ Nat] means for g be FinSequence of G st ( len g) <= $1 holds ( Product (g ^ (( Rev g) " ))) = ( 1_ G);

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A2: P[k];

        for g be FinSequence of G st ( len g) <= (k + 1) holds ( Product (g ^ (( Rev g) " ))) = ( 1_ G)

        proof

          let g be FinSequence of G;

          assume

           A3: ( len g) <= (k + 1);

          now

            per cases by A3, XXREAL_0: 1;

              case ( len g) < (k + 1);

              then ( len g) <= k by NAT_1: 13;

              hence thesis by A2;

            end;

              case

               A4: ( len g) = (k + 1);

              reconsider h = (g | k) as FinSequence of G;

              k < ( len g) by A4, NAT_1: 13;

              then

               A5: ( len h) = k by FINSEQ_1: 59;

              

               A6: ( Product ( <*(g /. (k + 1))*> ^ ( <*(g /. (k + 1))*> " ))) = (( Product <*(g /. (k + 1))*>) * ( Product ( <*(g /. (k + 1))*> " ))) by GROUP_4: 5

              .= ((g /. (k + 1)) * ( Product ( <*(g /. (k + 1))*> " ))) by FINSOP_1: 11

              .= ((g /. (k + 1)) * ( Product <*((g /. (k + 1)) " )*>)) by Th22

              .= ((g /. (k + 1)) * ((g /. (k + 1)) " )) by FINSOP_1: 11

              .= ( 1_ G) by GROUP_1:def 5;

              

               A7: g = (h ^ <*(g /. (k + 1))*>) by A4, FINSEQ_5: 21;

              then ( Rev g) = ( <*(g /. (k + 1))*> ^ ( Rev h)) by FINSEQ_5: 63;

              then (( Rev g) " ) = (( <*(g /. (k + 1))*> " ) ^ (( Rev h) " )) by Th21;

              

              then (g ^ (( Rev g) " )) = (h ^ ( <*(g /. (k + 1))*> ^ (( <*(g /. (k + 1))*> " ) ^ (( Rev h) " )))) by A7, FINSEQ_1: 32

              .= (h ^ (( <*(g /. (k + 1))*> ^ ( <*(g /. (k + 1))*> " )) ^ (( Rev h) " ))) by FINSEQ_1: 32;

              

              then ( Product (g ^ (( Rev g) " ))) = (( Product h) * ( Product (( <*(g /. (k + 1))*> ^ ( <*(g /. (k + 1))*> " )) ^ (( Rev h) " )))) by GROUP_4: 5

              .= (( Product h) * (( Product ( <*(g /. (k + 1))*> ^ ( <*(g /. (k + 1))*> " ))) * ( Product (( Rev h) " )))) by GROUP_4: 5

              .= (( Product h) * ( Product (( Rev h) " ))) by A6, GROUP_1:def 4

              .= ( Product (h ^ (( Rev h) " ))) by GROUP_4: 5;

              hence thesis by A2, A5;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      for g be FinSequence of G st ( len g) <= 0 holds ( Product (g ^ (( Rev g) " ))) = ( 1_ G)

      proof

        let g be FinSequence of G;

        assume ( len g) <= 0 ;

        then

         A8: g = ( <*> the carrier of G);

        then ( Rev g) = ( <*> the carrier of G) by FINSEQ_5: 79;

        then (( Rev g) " ) = ( <*> the carrier of G) by Th20;

        then (g ^ (( Rev g) " )) = ( <*> the carrier of G) by A8, FINSEQ_1: 34;

        hence thesis by GROUP_4: 8;

      end;

      then

       A9: P[ 0 ];

      for j be Nat holds P[j] from NAT_1:sch 2( A9, A1);

      then P[( len f)];

      hence thesis;

    end;

    theorem :: MATRIX_7:25

    

     Th24: for G be Group, f be FinSequence of G holds ( Product ((( Rev f) " ) ^ f)) = ( 1_ G)

    proof

      let G be Group, f be FinSequence of G;

      

       A1: ( len f) = ( len ( Rev f)) by FINSEQ_5:def 3;

      

       A2: ( len ( Rev (( Rev f) " ))) = ( len (( Rev (( Rev f) " )) " )) by Def3;

      then

       A3: ( dom ( Rev (( Rev f) " ))) = ( dom (( Rev (( Rev f) " )) " )) by FINSEQ_3: 29;

      

       A4: ( len (( Rev f) " )) = ( len ( Rev (( Rev f) " ))) by FINSEQ_5:def 3;

      

       A5: ( len ( Rev f)) = ( len (( Rev f) " )) by Def3;

      then

       A6: ( dom ( Rev f)) = ( dom (( Rev f) " )) by FINSEQ_3: 29;

      for i be Nat st 1 <= i & i <= ( len f) holds (f . i) = ((( Rev (( Rev f) " )) " ) . i)

      proof

        let i be Nat;

        assume that

         A7: 1 <= i and

         A8: i <= ( len f);

        ((( len f) - i) + 1) = ((( len f) -' i) + 1) by A8, XREAL_1: 233;

        then

        reconsider j = ((( len f) - i) + 1) as Nat;

        

         A9: (i + j) = (( len f) + 1);

        

         A10: i in ( Seg ( len f)) by A7, A8;

        then

         A11: i in ( dom (( Rev (( Rev f) " )) " )) by A1, A5, A4, A2, FINSEQ_1:def 3;

        (i - 1) >= 0 by A7, XREAL_1: 48;

        then (( len f) + 0 ) <= (( len f) + (i - 1)) by XREAL_1: 7;

        then

         A12: (( len f) - (i - 1)) <= ((( len f) + (i - 1)) - (i - 1)) by XREAL_1: 13;

        (( len f) - i) = (( len f) -' i) by A8, XREAL_1: 233;

        then ((( len f) - i) + 1) >= ( 0 + 1) by XREAL_1: 6;

        then j in ( Seg ( len f)) by A12;

        then

         A13: j in ( dom (( Rev f) " )) by A1, A5, FINSEQ_1:def 3;

        

         A14: (j + i) = (( len f) + 1);

        

         A15: i in ( dom f) by A10, FINSEQ_1:def 3;

        

        then (f . i) = (f /. i) by PARTFUN1:def 6

        .= (( Rev f) /. j) by A15, A9, FINSEQ_5: 66

        .= (((( Rev f) /. j) " ) " )

        .= (((( Rev f) " ) /. j) " ) by A6, A13, Def3

        .= ((( Rev (( Rev f) " )) /. i) " ) by A1, A5, A13, A14, FINSEQ_5: 66

        .= ((( Rev (( Rev f) " )) " ) /. i) by A3, A11, Def3

        .= ((( Rev (( Rev f) " )) " ) . i) by A11, PARTFUN1:def 6;

        hence thesis;

      end;

      then (( Rev (( Rev f) " )) " ) = f by A1, A5, A4, A2;

      hence thesis by Th23;

    end;

    theorem :: MATRIX_7:26

    

     Th25: for G be Group, f be FinSequence of G holds (( Product f) " ) = ( Product (( Rev f) " ))

    proof

      let G be Group, f be FinSequence of G;

      ( Product (f ^ (( Rev f) " ))) = ( 1_ G) by Th23;

      then

       A1: (( Product f) * ( Product (( Rev f) " ))) = ( 1_ G) by GROUP_4: 5;

      ( Product ((( Rev f) " ) ^ f)) = ( 1_ G) by Th24;

      then (( Product (( Rev f) " )) * ( Product f)) = ( 1_ G) by GROUP_4: 5;

      hence thesis by A1, GROUP_1: 5;

    end;

    theorem :: MATRIX_7:27

    

     Th26: for ITP be Element of ( Permutations n), ITG be Element of ( Group_of_Perm n) st ITG = ITP & n >= 1 holds (ITP " ) = (ITG " )

    proof

      let ITP be Element of ( Permutations n), ITG be Element of ( Group_of_Perm n);

      assume that

       A1: ITG = ITP and

       A2: n >= 1;

      reconsider qf = ITP as Function of ( Seg n), ( Seg n) by MATRIX_1:def 12;

      ( dom qf) = ( Seg n) by A2, FUNCT_2:def 1;

      then

       A3: ((ITP " ) * ITP) = ( id ( Seg n)) by FUNCT_1: 39;

      ITP is Permutation of ( Seg n) by MATRIX_1:def 12;

      then ( rng qf) = ( Seg n) by FUNCT_2:def 3;

      then

       A4: (ITP * (ITP " )) = ( id ( Seg n)) by FUNCT_1: 39;

      reconsider pf = (ITP " ) as Element of ( Group_of_Perm n) by MATRIX_1:def 13;

      

       A5: ( idseq n) = ( 1_ ( Group_of_Perm n)) & (ITG * pf) = (the multF of ( Group_of_Perm n) . (ITG,pf)) by MATRIX_1: 15;

      

       A6: (pf * ITG) = (the multF of ( Group_of_Perm n) . (pf,ITG));

      (the multF of ( Group_of_Perm n) . (ITG,pf)) = ((ITP " ) * ITP) & (the multF of ( Group_of_Perm n) . (pf,ITG)) = (ITP * (ITP " )) by A1, MATRIX_1:def 13;

      hence thesis by A3, A4, A5, A6, GROUP_1:def 5;

    end;

    

     Lm2: for n be Nat, IT be Element of ( Permutations n) st IT is even & n >= 1 holds (IT " ) is even

    proof

      let n be Nat, IT be Element of ( Permutations n);

      assume that

       A1: IT is even and

       A2: n >= 1;

      reconsider ITP = IT as Element of ( Permutations n);

      reconsider ITG = ITP as Element of ( Group_of_Perm n) by MATRIX_1:def 13;

      

       A3: ( len ( Permutations n)) = n by MATRIX_1: 9;

      then

      consider l be FinSequence of ( Group_of_Perm n) such that

       A4: (( len l) mod 2) = 0 and

       A5: IT = ( Product l) and

       A6: for i st i in ( dom l) holds ex q be Element of ( Permutations n) st (l . i) = q & q is being_transposition by A1;

      set m = ( len l);

      reconsider lv = (( Rev l) " ) as FinSequence of ( Group_of_Perm n);

      

       A7: ( len l) = ( len ( Rev l)) by FINSEQ_5:def 3;

      then

       A8: ( len l) = ( len lv) by Def3;

      

       A9: for i st i in ( dom lv) holds ex q2 be Element of ( Permutations n) st (lv . i) = q2 & q2 is being_transposition

      proof

        let i;

        reconsider ii = i as Nat;

        assume

         A10: i in ( dom lv);

        then

         A11: i in ( dom ( Rev l)) by A7, A8, FINSEQ_3: 29;

        

         A12: i in ( Seg ( len lv)) by A10, FINSEQ_1:def 3;

        then 1 <= i by FINSEQ_1: 1;

        then (m + 1) <= (m + i) by XREAL_1: 7;

        then

         A13: ((m + 1) - i) <= ((m + i) - i) by XREAL_1: 9;

        i <= m by A8, A12, FINSEQ_1: 1;

        then

         A14: (m - i) >= 0 by XREAL_1: 48;

        then ((m - i) + 1) = ((m -' i) + 1) by XREAL_0:def 2;

        then

        reconsider j = ((( len l) - i) + 1) as Nat;

        ((m - i) + 1) >= ( 0 + 1) by A14, XREAL_1: 7;

        then j in ( Seg ( len l)) by A13;

        then

         A15: j in ( dom l) by FINSEQ_1:def 3;

        then

        consider q be Element of ( Permutations n) such that

         A16: (l . j) = q and

         A17: q is being_transposition by A6;

        (lv . i) = (lv /. i) by A10, PARTFUN1:def 6;

        then

        reconsider qq = (lv . i) as Element of ( Permutations n) by MATRIX_1:def 13;

        reconsider qqf = qq as Function of ( Seg n), ( Seg n) by MATRIX_1:def 12;

        

         A18: (i + j) = (( len l) + 1);

        reconsider qf = q as Function of ( Seg n), ( Seg n) by MATRIX_1:def 12;

        consider i1,j1 be Nat such that

         A19: i1 in ( dom q) & j1 in ( dom q) & i1 <> j1 & (q . i1) = j1 & (q . j1) = i1 and

         A20: for k be Nat st k <> i1 & k <> j1 & k in ( dom q) holds (q . k) = k by A17;

        

         A21: ( dom qf) = ( Seg n) & ( dom qqf) = ( Seg n) by A2, FUNCT_2:def 1;

        

         A22: qq = ((( Rev l) " ) /. i) by A10, PARTFUN1:def 6

        .= ((( Rev l) /. ii) " ) by A11, Def3

        .= ((l /. j) " ) by A18, A15, FINSEQ_5: 66

        .= (q " ) by A2, A15, A16, Th26, PARTFUN1:def 6;

        

         A23: for k be Nat st k <> j1 & k <> i1 & k in ( dom qq) holds (qq . k) = k

        proof

          let k be Nat;

          assume that

           A24: k <> j1 & k <> i1 and

           A25: k in ( dom qq);

          (q . k) = k by A20, A21, A24, A25;

          hence thesis by A21, A22, A25, FUNCT_1: 32;

        end;

        

         A26: qq = ((( Rev l) " ) /. i) by A10, PARTFUN1:def 6

        .= ((( Rev l) /. ii) " ) by A11, Def3

        .= ((l /. j) " ) by A18, A15, FINSEQ_5: 66

        .= (q " ) by A2, A15, A16, Th26, PARTFUN1:def 6;

        ex i, j st i in ( dom qq) & j in ( dom qq) & i <> j & (qq . i) = j & (qq . j) = i & for k st k <> i & k <> j & k in ( dom qq) holds (qq . k) = k

        proof

          take i = i1, j = j1;

          thus i in ( dom qq) & j in ( dom qq) & i <> j & (qq . i) = j & (qq . j) = i by A19, A21, A26, FUNCT_1: 32;

          let k;

          thus thesis by A23;

        end;

        then qq is being_transposition;

        hence thesis;

      end;

      (ITG " ) = (ITP " ) by A2, Th26;

      then (IT " ) = ( Product lv) by A5, Th25;

      hence thesis by A3, A4, A8, A9;

    end;

    theorem :: MATRIX_7:28

    

     Th27: for n be Nat, IT be Element of ( Permutations n) st n >= 1 holds IT is even iff (IT " ) is even

    proof

      let n be Nat, IT be Element of ( Permutations n);

      assume

       A1: n >= 1;

      hence IT is even implies (IT " ) is even by Lm2;

      now

        assume (IT " ) is even;

        then ((IT " ) " ) is even by A1, Lm2;

        hence IT is even by FUNCT_1: 43;

      end;

      hence thesis;

    end;

    theorem :: MATRIX_7:29

    

     Th28: for n be Nat, K be commutative Ring, p be Element of ( Permutations n), x be Element of K st n >= 1 holds ( - (x,p)) = ( - (x,(p " )))

    proof

      let n be Nat, K be commutative Ring, p be Element of ( Permutations n), x be Element of K;

      assume

       A1: n >= 1;

      reconsider pf = p as Permutation of ( Seg n) by MATRIX_1:def 12;

      

       A2: ( len ( Permutations n)) = n by MATRIX_1: 9;

      per cases ;

        suppose p is even;

        then ( - (x,p)) = x & (pf " ) is even by A1, A2, Th27, MATRIX_1:def 16;

        hence thesis by A2, MATRIX_1:def 16;

      end;

        suppose not p is even;

        then ( - (x,p)) = ( - x) & not (p " ) is even by A1, Th27, MATRIX_1:def 16;

        hence thesis by MATRIX_1:def 16;

      end;

    end;

    theorem :: MATRIX_7:30

    for K be commutative Ring, f1,f2 be FinSequence of K holds (the multF of K $$ (f1 ^ f2)) = ((the multF of K $$ f1) * (the multF of K $$ f2)) by FINSOP_1: 5;

    theorem :: MATRIX_7:31

    

     Th30: for K be commutative Ring, R1,R2 be FinSequence of K st (R1,R2) are_fiberwise_equipotent holds (the multF of K $$ R1) = (the multF of K $$ R2)

    proof

      let K be commutative Ring;

      defpred P[ Nat] means for f,g be FinSequence of K st (f,g) are_fiberwise_equipotent & ( len f) = $1 holds (the multF of K $$ f) = (the multF of K $$ g);

      let R1,R2 be FinSequence of K;

      assume

       A1: (R1,R2) are_fiberwise_equipotent ;

      

       A2: ( len R1) = ( len R1);

      

       A3: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A4: P[n];

        reconsider n1 = n as Nat;

        let f,g be FinSequence of K;

        assume that

         A5: (f,g) are_fiberwise_equipotent and

         A6: ( len f) = (n + 1);

        

         A7: ( rng f) c= the carrier of K by FINSEQ_1:def 4;

        ( 0 + 1) <= (n + 1) by NAT_1: 13;

        then

         A8: (n + 1) in ( dom f) by A6, FINSEQ_3: 25;

        then (f . (n + 1)) in ( rng f) by FUNCT_1:def 3;

        then

        reconsider a = (f . (n + 1)) as Element of K by A7;

        ( rng f) = ( rng g) by A5, CLASSES1: 75;

        then a in ( rng g) by A8, FUNCT_1:def 3;

        then

        consider m be Nat such that

         A9: m in ( dom g) and

         A10: (g . m) = a by FINSEQ_2: 10;

        

         A11: g = ((g | m) ^ (g /^ m)) by RFINSEQ: 8;

        set gg = (g /^ m), gm = (g | m);

        

         A12: 1 <= m by A9, FINSEQ_3: 25;

        then ( max ( 0 ,(m - 1))) = (m - 1) by FINSEQ_2: 4;

        then

        reconsider m1 = (m - 1) as Nat by FINSEQ_2: 5;

        m in ( Seg m) by A12;

        then

         A13: (gm . m) = a by A9, A10, RFINSEQ: 6;

        

         A14: m = (m1 + 1);

        then m1 <= m by NAT_1: 11;

        then

         A15: ( Seg m1) c= ( Seg m) by FINSEQ_1: 5;

        m <= ( len g) by A9, FINSEQ_3: 25;

        then ( len gm) = m by FINSEQ_1: 59;

        then

         A16: gm = ((gm | m1) ^ <*a*>) by A14, A13, RFINSEQ: 7;

        set fn = (f | n1);

        

         A17: f = (fn ^ <*a*>) by A6, RFINSEQ: 7;

        

         A18: (gm | m1) = (g | (( Seg m) /\ ( Seg m1))) by RELAT_1: 71

        .= (g | m1) by A15, XBOOLE_1: 28;

        now

          let x be object;

          ( card ( Coim (f,x))) = ( card ( Coim (g,x))) by A5, CLASSES1:def 10;

          

          then (( card (fn " {x})) + ( card ( <*a*> " {x}))) = ( card ((((g | m1) ^ <*a*>) ^ (g /^ m)) " {x})) by A11, A16, A18, A17, FINSEQ_3: 57

          .= (( card (((g | m1) ^ <*a*>) " {x})) + ( card ((g /^ m) " {x}))) by FINSEQ_3: 57

          .= ((( card ((g | m1) " {x})) + ( card ( <*a*> " {x}))) + ( card ((g /^ m) " {x}))) by FINSEQ_3: 57

          .= ((( card ((g | m1) " {x})) + ( card ((g /^ m) " {x}))) + ( card ( <*a*> " {x})))

          .= (( card (((g | m1) ^ (g /^ m)) " {x})) + ( card ( <*a*> " {x}))) by FINSEQ_3: 57;

          hence ( card ( Coim (fn,x))) = ( card ( Coim (((g | m1) ^ (g /^ m)),x)));

        end;

        then

         A19: (fn,((g | m1) ^ (g /^ m))) are_fiberwise_equipotent by CLASSES1:def 10;

        ( len fn) = n by A6, FINSEQ_1: 59, NAT_1: 11;

        then (the multF of K $$ fn) = (the multF of K $$ ((g | m1) ^ gg)) by A4, A19;

        

        hence (the multF of K $$ f) = ((the multF of K $$ ((g | m1) ^ gg)) * (the multF of K $$ <*a*>)) by A17, FINSOP_1: 5

        .= (((the multF of K $$ (g | m1)) * (the multF of K $$ gg)) * (the multF of K $$ <*a*>)) by FINSOP_1: 5

        .= (((the multF of K $$ (g | m1)) * (the multF of K $$ <*a*>)) * (the multF of K $$ gg)) by GROUP_1:def 3

        .= ((the multF of K $$ gm) * (the multF of K $$ gg)) by A16, A18, FINSOP_1: 5

        .= (the multF of K $$ g) by A11, FINSOP_1: 5;

      end;

      

       A20: P[ 0 ]

      proof

        let f,g be FinSequence of K;

        assume (f,g) are_fiberwise_equipotent & ( len f) = 0 ;

        then

         A21: ( len g) = 0 & f = ( <*> the carrier of K) by RFINSEQ: 3;

        then g = ( <*> the carrier of K);

        hence thesis by A21;

      end;

      for n holds P[n] from NAT_1:sch 2( A20, A3);

      hence thesis by A1, A2;

    end;

    theorem :: MATRIX_7:32

    

     Th31: for n be Nat, K be commutative Ring, p be Element of ( Permutations n), f,g be FinSequence of K st ( len f) = n & g = (f * p) holds (f,g) are_fiberwise_equipotent

    proof

      let n be Nat, K be commutative Ring, p be Element of ( Permutations n), f,g be FinSequence of K;

      assume that

       A1: ( len f) = n and

       A2: g = (f * p);

      reconsider fp = p as Function of ( Seg n), ( Seg n) by MATRIX_1:def 12;

      

       A3: p is Permutation of ( Seg n) by MATRIX_1:def 12;

      then

       A4: ( rng p) = ( Seg n) by FUNCT_2:def 3;

      ( rng fp) = ( Seg n) by A3, FUNCT_2:def 3;

      then ( rng p) c= ( dom f) by A1, FINSEQ_1:def 3;

      then

       A5: ( dom (f * p)) = ( dom fp) by RELAT_1: 27;

      ( dom f) = ( Seg n) by A1, FINSEQ_1:def 3;

      hence thesis by A2, A5, A4, CLASSES1: 77;

    end;

    theorem :: MATRIX_7:33

    for n be Nat, K be commutative Ring, p be Element of ( Permutations n), f,g be FinSequence of K st n >= 1 & ( len f) = n & g = (f * p) holds (the multF of K $$ f) = (the multF of K $$ g) by Th30, Th31;

    theorem :: MATRIX_7:34

    

     Th33: for n be Nat, K be Ring, p be Element of ( Permutations n), f be FinSequence of K st n >= 1 & ( len f) = n holds (f * p) is FinSequence of K

    proof

      let n be Nat, K be Ring, p be Element of ( Permutations n), f be FinSequence of K;

      assume that

       A1: n >= 1 and

       A2: ( len f) = n;

      reconsider q = p as Function of ( Seg n), ( Seg n) by MATRIX_1:def 12;

      p is bijective Function of ( Seg n), ( Seg n) by MATRIX_1:def 12;

      then ( rng q) = ( Seg n) by FUNCT_2:def 3;

      then ( rng p) c= ( dom f) by A2, FINSEQ_1:def 3;

      

      then ( dom (f * p)) = ( dom q) by RELAT_1: 27

      .= ( Seg n) by A1, FUNCT_2:def 1;

      then

      reconsider h = (f * p) as FinSequence by FINSEQ_1:def 2;

      ( rng h) c= ( rng f) & ( rng f) c= the carrier of K by FINSEQ_1:def 4, RELAT_1: 26;

      then ( rng h) c= the carrier of K;

      hence thesis by FINSEQ_1:def 4;

    end;

    theorem :: MATRIX_7:35

    

     Th34: for n be Nat, K be commutative Ring, p be Element of ( Permutations n), A be Matrix of n, K st n >= 1 holds ( Path_matrix ((p " ),(A @ ))) = (( Path_matrix (p,A)) * (p " ))

    proof

      let n be Nat, K be commutative Ring, p be Element of ( Permutations n), A be Matrix of n, K;

      set f = ( Path_matrix (p,A));

      reconsider fp = (p " ) as Function of ( Seg n), ( Seg n) by MATRIX_1:def 12;

      reconsider fp0 = p as Function of ( Seg n), ( Seg n) by MATRIX_1:def 12;

      assume

       A1: n >= 1;

      then

       A2: ( dom fp) = ( Seg n) by FUNCT_2:def 1;

      

       A3: ( len ( Path_matrix (p,A))) = n by MATRIX_3:def 7;

      then

      reconsider m = (( Path_matrix (p,A)) * (p " )) as FinSequence of K by A1, Th33;

      (p " ) is Permutation of ( Seg n) by MATRIX_1:def 12;

      then

       A4: ( rng fp) = ( Seg n) by FUNCT_2:def 3;

      then ( rng (p " )) c= ( dom f) by A3, FINSEQ_1:def 3;

      then

       A5: ( dom (f * (p " ))) = ( dom fp) by RELAT_1: 27;

      

       A6: p is Permutation of ( Seg n) by MATRIX_1:def 12;

      

       A7: for i, j st i in ( dom m) & j = ((p " ) . i) holds (m . i) = ((A @ ) * (i,j))

      proof

        let i, j;

        assume that

         A8: i in ( dom m) and

         A9: j = ((p " ) . i);

        

         A10: j in ( Seg n) by A4, A5, A8, A9, FUNCT_1:def 3;

        then

         A11: j in ( dom f) by A3, FINSEQ_1:def 3;

        ( rng fp0) = ( Seg n) by A6, FUNCT_2:def 3;

        then i = (p . j) by A5, A2, A8, A9, FUNCT_1: 32;

        then

         A12: (( Path_matrix (p,A)) . j) = (A * (j,i)) by A11, MATRIX_3:def 7;

        

         A13: ( dom A) = ( Seg ( len A)) by FINSEQ_1:def 3

        .= ( Seg n) by MATRIX_0:def 2;

        ( len A) = n by MATRIX_0:def 2;

        then i in ( Seg ( width A)) by A1, A5, A2, A8, MATRIX_0: 20;

        then

         A14: [j, i] in ( Indices A) by A10, A13, ZFMISC_1:def 2;

        ((( Path_matrix (p,A)) * (p " )) . i) = (( Path_matrix (p,A)) . ((p " ) . i)) by A5, A8, FUNCT_1: 13;

        hence thesis by A9, A12, A14, MATRIX_0:def 6;

      end;

      n in NAT by ORDINAL1:def 12;

      then ( len m) = n by A5, A2, FINSEQ_1:def 3;

      hence thesis by A7, MATRIX_3:def 7;

    end;

    theorem :: MATRIX_7:36

    

     Th35: for n be Nat, K be commutative Ring, p be Element of ( Permutations n), A be Matrix of n, K st n >= 1 holds (( Path_product (A @ )) . (p " )) = (( Path_product A) . p)

    proof

      let n be Nat, K be commutative Ring, p be Element of ( Permutations n), A be Matrix of n, K;

      assume

       A1: n >= 1;

      

       A2: ( len ( Path_matrix (p,A))) = n by MATRIX_3:def 7;

      then

      reconsider g = (( Path_matrix (p,A)) * (p " )) as FinSequence of K by A1, Th33;

      (( Path_product (A @ )) . (p " )) = ( - ((the multF of K $$ ( Path_matrix ((p " ),(A @ )))),(p " ))) by MATRIX_3:def 8

      .= ( - ((the multF of K $$ g),(p " ))) by A1, Th34

      .= ( - ((the multF of K $$ g),p)) by A1, Th28

      .= ( - ((the multF of K $$ ( Path_matrix (p,A))),p)) by A2, Th30, Th31;

      hence thesis by MATRIX_3:def 8;

    end;

    theorem :: MATRIX_7:37

    for n be Nat, K be commutative Ring, A be Matrix of n, K st n >= 1 holds ( Det A) = ( Det (A @ ))

    proof

      let n be Nat, K be commutative Ring, A be Matrix of n, K;

      set f = ( Path_product A);

      set f2 = ( Path_product (A @ ));

      set F = the addF of K;

      set Y = the carrier of K;

      set X = ( Permutations n);

      set B = ( In (X,( Fin X)));

      set I = (the addF of K $$ (B,( Path_product (A @ ))));

      

       A1: ( Det A) = (the addF of K $$ (B,( Path_product A))) by MATRIX_3:def 9;

      X in ( Fin X) by FINSUB_1:def 5;

      then

       A2: B = ( Permutations n) by SUBSET_1:def 8;

      

       A3: { (p " ) where p be Permutation of ( Seg n) : p in B } c= B

      proof

        let z be object;

        assume z in { (p " ) where p be Permutation of ( Seg n) : p in B };

        then ex p be Permutation of ( Seg n) st z = (p " ) & p in B;

        hence thesis by A2, MATRIX_1:def 12;

      end;

      

       A4: B c= { (p " ) where p be Permutation of ( Seg n) : p in B }

      proof

        let z be object;

        assume z in B;

        then

        reconsider q2 = z as Permutation of ( Seg n) by A2, MATRIX_1:def 12;

        set q3 = (q2 " );

        (q3 " ) = q2 & q3 in B by A2, FUNCT_1: 43, MATRIX_1:def 12;

        hence thesis;

      end;

      X in ( Fin X) by FINSUB_1:def 5;

      then

       A5: B <> {} or F is having_a_unity by SUBSET_1:def 8;

      then

      consider G0 be Function of ( Fin X), Y such that

       A6: I = (G0 . B) and

       A7: for e be Element of Y st e is_a_unity_wrt F holds (G0 . {} ) = e and

       A8: for x be Element of X holds (G0 . {x}) = (f2 . x) and

       A9: for B9 be Element of ( Fin X) st B9 c= B & B9 <> {} holds for x be Element of X st x in (B \ B9) holds (G0 . (B9 \/ {x})) = (F . ((G0 . B9),(f2 . x))) by SETWISEO:def 3;

      deffunc F8( set) = (G0 . { (p " ) where p be Permutation of ( Seg n) : p in $1 });

      

       A10: for x2 be set st x2 in ( Fin X) holds F8(x2) in Y

      proof

        let x2 be set;

        assume x2 in ( Fin X);

        { (p " ) where p be Permutation of ( Seg n) : p in x2 } c= X

        proof

          let r be object;

          assume r in { (p " ) where p be Permutation of ( Seg n) : p in x2 };

          then ex p be Permutation of ( Seg n) st r = (p " ) & p in x2;

          hence thesis by MATRIX_1:def 12;

        end;

        then { (p " ) where p be Permutation of ( Seg n) : p in x2 } is Element of ( Fin X) by FINSUB_1: 17;

        hence thesis by FUNCT_2: 5;

      end;

      consider G1 be Function of ( Fin X), Y such that

       A11: for x5 be set st x5 in ( Fin X) holds (G1 . x5) = F8(x5) from FUNCT_2:sch 11( A10);

      assume

       A12: n >= 1;

      

       A13: for x be Element of X holds (G1 . {x}) = (f . x)

      proof

        let x be Element of X;

        reconsider B4 = {.x.} as Element of ( Fin X);

        reconsider q = x as Permutation of ( Seg n) by MATRIX_1:def 12;

        

         A14: (q " ) is Element of X by MATRIX_1:def 12;

        

         A15: { (p " ) where p be Permutation of ( Seg n) : p in B4 } c= {(q " )}

        proof

          let z be object;

          assume z in { (p " ) where p be Permutation of ( Seg n) : p in B4 };

          then

          consider p be Permutation of ( Seg n) such that

           A16: z = (p " ) and

           A17: p in B4;

          p = x by A17, TARSKI:def 1;

          hence thesis by A16, TARSKI:def 1;

        end;

         {(q " )} c= { (p " ) where p be Permutation of ( Seg n) : p in B4 }

        proof

          let z be object;

          assume z in {(q " )};

          then q in B4 & z = (q " ) by TARSKI:def 1;

          hence thesis;

        end;

        then { (p " ) where p be Permutation of ( Seg n) : p in B4 } = {(q " )} by A15;

        

        then (G1 . B4) = (G0 . {(q " )}) by A11

        .= (f2 . (q " )) by A8, A14

        .= (( Path_product A) . q) by A12, Th35;

        hence thesis;

      end;

      

       A18: for B9 be Element of ( Fin X) st B9 c= B & B9 <> {} holds for x be Element of X st x in (B \ B9) holds (G1 . (B9 \/ {x})) = (F . ((G1 . B9),(f . x)))

      proof

        let B9 be Element of ( Fin X);

        assume that

         A19: B9 c= B and

         A20: B9 <> {} ;

        thus for x be Element of X st x in (B \ B9) holds (G1 . (B9 \/ {x})) = (F . ((G1 . B9),(f . x)))

        proof

          { (p " ) where p be Permutation of ( Seg n) : p in B9 } c= X

          proof

            let v be object;

            assume v in { (p " ) where p be Permutation of ( Seg n) : p in B9 };

            then ex p be Permutation of ( Seg n) st (p " ) = v & p in B9;

            hence thesis by MATRIX_1:def 12;

          end;

          then

          reconsider B2 = { (p " ) where p be Permutation of ( Seg n) : p in B9 } as Element of ( Fin X) by FINSUB_1: 17;

          set d = the Element of B9;

          let x be Element of X;

          reconsider px = x as Permutation of ( Seg n) by MATRIX_1:def 12;

          reconsider y = (px " ) as Element of X by MATRIX_1:def 12;

          

           A21: (B2 \/ {y}) c= { (p " ) where p be Permutation of ( Seg n) : p in (B9 \/ {x}) }

          proof

            let z be object;

            assume z in (B2 \/ {y});

            then

             A22: z in B2 or z in {y} by XBOOLE_0:def 3;

            now

              per cases by A22, TARSKI:def 1;

                case z in B2;

                then

                consider p be Permutation of ( Seg n) such that

                 A23: z = (p " ) and

                 A24: p in B9;

                p in (B9 \/ {x}) by A24, XBOOLE_0:def 3;

                hence thesis by A23;

              end;

                case

                 A25: z = y;

                px in {x} by TARSKI:def 1;

                then px in (B9 \/ {x}) by XBOOLE_0:def 3;

                hence thesis by A25;

              end;

            end;

            hence thesis;

          end;

          

           A26: B2 c= B

          proof

            let u be object;

            assume u in B2;

            then ex p be Permutation of ( Seg n) st (p " ) = u & p in B9;

            hence thesis by A2, MATRIX_1:def 12;

          end;

          assume x in (B \ B9);

          then

           A27: not x in B9 by XBOOLE_0:def 5;

          now

            assume y in B2;

            then

            consider pp be Permutation of ( Seg n) such that

             A28: y = (pp " ) and

             A29: pp in B9;

            px = ((pp " ) " ) by A28, FUNCT_1: 43;

            hence contradiction by A27, A29, FUNCT_1: 43;

          end;

          then

           A30: y in (B \ B2) by A2, XBOOLE_0:def 5;

          d in B by A19, A20;

          then

          reconsider pd = d as Permutation of ( Seg n) by A2, MATRIX_1:def 12;

          

           A31: (pd " ) in B2 by A20;

          

           A32: (G1 . (B9 \/ {.x.})) = (G0 . { (p " ) where p be Permutation of ( Seg n) : p in (B9 \/ {x}) }) & (G0 . B2) = (G1 . B9) by A11;

          { (p " ) where p be Permutation of ( Seg n) : p in (B9 \/ {x}) } c= (B2 \/ {y})

          proof

            let z be object;

            assume z in { (p " ) where p be Permutation of ( Seg n) : p in (B9 \/ {x}) };

            then

            consider p be Permutation of ( Seg n) such that

             A33: z = (p " ) and

             A34: p in (B9 \/ {x});

            now

              per cases by A34, XBOOLE_0:def 3;

                case p in B9;

                hence z in B2 or z in {y} by A33;

              end;

                case p in {x};

                then p = x by TARSKI:def 1;

                hence z in B2 or z in {y} by A33, TARSKI:def 1;

              end;

            end;

            hence thesis by XBOOLE_0:def 3;

          end;

          then (B2 \/ {y}) = { (p " ) where p be Permutation of ( Seg n) : p in (B9 \/ {x}) } by A21;

          then (G0 . { (p " ) where p be Permutation of ( Seg n) : p in (B9 \/ {x}) }) = (F . ((G0 . B2),(f2 . y))) by A9, A26, A31, A30;

          hence thesis by A12, A32, Th35;

        end;

      end;

      

       A35: for e be Element of Y st e is_a_unity_wrt F holds (G1 . {} ) = e

      proof

         {} is Subset of X by SUBSET_1: 1;

        then

        reconsider B3 = {} as Element of ( Fin X) by FINSUB_1: 17;

        let e be Element of Y;

        { (p " ) where p be Permutation of ( Seg n) : p in B3 } c= {}

        proof

          let s be object;

          assume s in { (p " ) where p be Permutation of ( Seg n) : p in B3 };

          then ex p be Permutation of ( Seg n) st s = (p " ) & p in B3;

          hence thesis;

        end;

        then

         A36: { (p " ) where p be Permutation of ( Seg n) : p in B3 } = {} ;

        assume e is_a_unity_wrt F;

        then (G0 . { (p " ) where p be Permutation of ( Seg n) : p in B3 }) = e by A7, A36;

        hence thesis by A11;

      end;

      (G1 . B) = (G0 . { (p " ) where p be Permutation of ( Seg n) : p in B }) by A11;

      then I = (G1 . B) by A6, A3, A4, XBOOLE_0:def 10;

      then (the addF of K $$ (( In (( Permutations n),( Fin ( Permutations n)))),( Path_product A))) = (the addF of K $$ (( In (( Permutations n),( Fin ( Permutations n)))),( Path_product (A @ )))) by A5, A35, A13, A18, SETWISEO:def 3;

      hence thesis by A1, MATRIX_3:def 9;

    end;