matrix11.miz



    begin

    reserve x,y for object,

X for set,

i,j,k,l,n,m for Nat,

D for non empty set,

K for commutative Ring,

a,b for Element of K,

perm,p,q for Element of ( Permutations n),

Perm,P for Permutation of ( Seg n),

F for Function of ( Seg n), ( Seg n),

perm2,p2,q2,pq2 for Element of ( Permutations (n + 2)),

Perm2 for Permutation of ( Seg (n + 2));

    notation

      let X be set;

      synonym 2Set (X) for TWOELEMENTSETS (X);

    end

    theorem :: MATRIX11:1

    

     Th1: X in ( 2Set ( Seg n)) iff ex i, j st i in ( Seg n) & j in ( Seg n) & i < j & X = {i, j}

    proof

      thus X in ( 2Set ( Seg n)) implies ex i, j st i in ( Seg n) & j in ( Seg n) & i < j & X = {i, j}

      proof

        assume X in ( 2Set ( Seg n));

        then

        consider x,y be object such that

         A1: x in ( Seg n) and

         A2: y in ( Seg n) and

         A3: x <> y and

         A4: X = {x, y} by SGRAPH1: 8;

        reconsider x, y as Element of NAT by A1, A2;

        x > y or y > x by A3, XXREAL_0: 1;

        hence thesis by A1, A2, A4;

      end;

      assume ex i, j st i in ( Seg n) & j in ( Seg n) & i < j & X = {i, j};

      then

      consider i, j such that

       A5: i in ( Seg n) and

       A6: j in ( Seg n) and

       A7: i < j and

       A8: X = {i, j};

       {i, j} c= ( Seg n) by A5, A6, ZFMISC_1: 32;

      hence thesis by A5, A6, A7, A8, SGRAPH1: 8;

    end;

    theorem :: MATRIX11:2

    

     Th2: ( 2Set ( Seg 0 )) = {} & ( 2Set ( Seg 1)) = {} by FINSEQ_1: 2;

    theorem :: MATRIX11:3

    

     Th3: for n st n >= 2 holds {1, 2} in ( 2Set ( Seg n))

    proof

      let n such that

       A1: n >= 2;

      1 <= n by A1, XXREAL_0: 2;

      then

       A2: 1 in ( Seg n);

      2 in ( Seg n) by A1;

      hence thesis by A2, Th1;

    end;

    registration

      let n;

      cluster ( 2Set ( Seg (n + 2))) -> non empty finite;

      coherence

      proof

        (n + 2) >= ( 0 + 2) by XREAL_1: 6;

        hence thesis by Th3;

      end;

    end

    registration

      let n, x;

      let perm be Element of ( Permutations n);

      cluster (perm . x) -> natural;

      coherence

      proof

        per cases ;

          suppose

           A1: x in ( dom perm);

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

          then

           A2: ( rng perm) = ( Seg n) by FUNCT_2:def 3;

          (perm . x) in ( rng perm) by A1, FUNCT_1:def 3;

          hence thesis by A2;

        end;

          suppose not x in ( dom perm);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let K;

      cluster the multF of K -> having_a_unity;

      coherence ;

      cluster the multF of K -> associative;

      coherence ;

    end

    definition

      let n, K;

      let perm2 be Element of ( Permutations (n + 2));

      :: MATRIX11:def1

      func Part_sgn (perm2,K) -> Function of ( 2Set ( Seg (n + 2))), the carrier of K means

      : Def1: for i,j be Nat st i in ( Seg (n + 2)) & j in ( Seg (n + 2)) & i < j holds ((perm2 . i) < (perm2 . j) implies (it . {i, j}) = ( 1_ K)) & ((perm2 . i) > (perm2 . j) implies (it . {i, j}) = ( - ( 1_ K)));

      existence

      proof

        set n9 = (n + 2);

        defpred P[ object, object] means for i,j be Element of NAT st i in ( Seg n9) & j in ( Seg n9) & i < j & $1 = {i, j} holds ((perm2 . i) < (perm2 . j) implies $2 = ( 1_ K)) & ((perm2 . i) > (perm2 . j) implies $2 = ( - ( 1_ K)));

        

         A1: for x be object st x in ( 2Set ( Seg n9)) holds ex y be object st y in the carrier of K & P[x, y]

        proof

          let x be object;

          assume x in ( 2Set ( Seg n9));

          then

          consider i, j such that

           A2: i in ( Seg n9) and

           A3: j in ( Seg n9) and

           A4: i < j and

           A5: x = {i, j} by Th1;

          perm2 is Permutation of ( Seg n9) by MATRIX_1:def 12;

          then

           A6: (perm2 . i) <> (perm2 . j) by A2, A3, A4, FUNCT_2: 19;

          now

            per cases by A6, XXREAL_0: 1;

              case

               A7: (perm2 . i) < (perm2 . j);

               P[x, ( 1_ K)]

              proof

                let i9,j9 be Element of NAT such that i9 in ( Seg n9) and j9 in ( Seg n9) and

                 A8: i9 < j9 and

                 A9: x = {i9, j9};

                i = i9 & j = j9 or i = j9 & j = i9 by A5, A9, ZFMISC_1: 22;

                hence thesis by A4, A7, A8;

              end;

              hence thesis;

            end;

              case

               A10: (perm2 . i) > (perm2 . j);

               P[x, ( - ( 1_ K))]

              proof

                let i9,j9 be Element of NAT such that i9 in ( Seg n9) and j9 in ( Seg n9) and

                 A11: i9 < j9 and

                 A12: x = {i9, j9};

                i = i9 & j = j9 or i = j9 & j = i9 by A5, A12, ZFMISC_1: 22;

                hence thesis by A4, A10, A11;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        consider Path be Function of ( 2Set ( Seg n9)), the carrier of K such that

         A13: for x be object st x in ( 2Set ( Seg n9)) holds P[x, (Path . x)] from FUNCT_2:sch 1( A1);

        take Path;

        let i,j be Nat such that

         A14: i in ( Seg n9) and

         A15: j in ( Seg n9) and

         A16: i < j;

         {i, j} in ( 2Set ( Seg n9)) by A14, A15, A16, Th1;

        hence thesis by A13, A14, A15, A16;

      end;

      uniqueness

      proof

        set n9 = (n + 2);

        let P1,P2 be Function of ( 2Set ( Seg n9)), the carrier of K such that

         A17: for i,j be Nat st i in ( Seg n9) & j in ( Seg n9) & i < j holds ((perm2 . i) < (perm2 . j) implies (P1 . {i, j}) = ( 1_ K)) & ((perm2 . i) > (perm2 . j) implies (P1 . {i, j}) = ( - ( 1_ K))) and

         A18: for i,j be Nat st i in ( Seg n9) & j in ( Seg n9) & i < j holds ((perm2 . i) < (perm2 . j) implies (P2 . {i, j}) = ( 1_ K)) & ((perm2 . i) > (perm2 . j) implies (P2 . {i, j}) = ( - ( 1_ K)));

        for x be object st x in ( 2Set ( Seg n9)) holds (P1 . x) = (P2 . x)

        proof

          let x be object;

          assume x in ( 2Set ( Seg n9));

          then

          consider i, j such that

           A19: i in ( Seg n9) and

           A20: j in ( Seg n9) and

           A21: i < j and

           A22: x = {i, j} by Th1;

          perm2 is Permutation of ( Seg n9) by MATRIX_1:def 12;

          then

           A23: (perm2 . i) <> (perm2 . j) by A19, A20, A21, FUNCT_2: 19;

          now

            per cases by A23, XXREAL_0: 1;

              case

               A24: (perm2 . i) < (perm2 . j);

              then (P1 . {i, j}) = ( 1_ K) by A17, A19, A20, A21;

              hence thesis by A18, A19, A20, A21, A22, A24;

            end;

              case

               A25: (perm2 . i) > (perm2 . j);

              then (P1 . {i, j}) = ( - ( 1_ K)) by A17, A19, A20, A21;

              hence thesis by A18, A19, A20, A21, A22, A25;

            end;

          end;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: MATRIX11:4

    

     Th4: for X be Element of ( Fin ( 2Set ( Seg (n + 2)))) st for x st x in X holds (( Part_sgn (p2,K)) . x) = ( 1_ K) holds (the multF of K $$ (X,( Part_sgn (p2,K)))) = ( 1_ K)

    proof

      let X be Element of ( Fin ( 2Set ( Seg (n + 2)))) such that

       A1: for x st x in X holds (( Part_sgn (p2,K)) . x) = ( 1_ K);

      set Path = ( Part_sgn (p2,K));

      set 2S = ( 2Set ( Seg (n + 2)));

      set KK = the carrier of K;

      set mm = the multF of K;

      consider G be Function of ( Fin 2S), KK such that

       A2: (mm $$ (X,Path)) = (G . X) and

       A3: for e be Element of KK st e is_a_unity_wrt mm holds (G . {} ) = e and

       A4: for x be Element of 2S holds (G . {x}) = (Path . x) and

       A5: for B be Element of ( Fin 2S) st B c= X & B <> {} holds for x be Element of 2S st x in (X \ B) holds (G . (B \/ {x})) = (mm . ((G . B),(Path . x))) by SETWISEO:def 3;

      defpred P[ Nat] means for B be Element of ( Fin 2S) st ( card B) = $1 & B c= X holds (G . B) = ( 1_ K);

      

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

      proof

        let k be Nat such that

         A7: P[k];

        set k1 = (k + 1);

        let B be Element of ( Fin 2S) such that

         A8: ( card B) = k1 and

         A9: B c= X;

        now

          per cases ;

            case k = 0 ;

            then

            consider x be object such that

             A10: B = {x} by A8, CARD_2: 42;

            

             A11: x in B by A10, TARSKI:def 1;

            B c= 2S by FINSUB_1:def 5;

            then

            reconsider x as Element of 2S by A11;

            (G . B) = (Path . x) by A4, A10;

            hence thesis by A1, A9, A11;

          end;

            case

             A12: k > 0 ;

            consider x be object such that

             A13: x in B by A8, CARD_1: 27, XBOOLE_0:def 1;

            B c= 2S by FINSUB_1:def 5;

            then

            reconsider x as Element of 2S by A13;

            

             A14: (Path . x) = ( 1_ K) by A1, A9, A13;

            B c= 2S by FINSUB_1:def 5;

            then (B \ {x}) c= 2S;

            then

            reconsider B9 = (B \ {x}) as Element of ( Fin 2S) by FINSUB_1:def 5;

            

             A15: not x in B9 by ZFMISC_1: 56;

            then

             A16: x in (X \ B9) by A9, A13, XBOOLE_0:def 5;

            

             A17: ( {x} \/ B9) = B by A13, ZFMISC_1: 116;

            then

             A18: (k + 1) = (( card B9) + 1) by A8, A15, CARD_2: 41;

            then (G . B9) = ( 1_ K) by A7, A9, XBOOLE_1: 1;

            then (G . B) = (( 1_ K) * ( 1_ K)) by A5, A9, A12, A17, A18, A16, A14, CARD_1: 27, XBOOLE_1: 1;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A19: P[ 0 ]

      proof

        let B be Element of ( Fin 2S) such that

         A20: ( card B) = 0 and B c= X;

        B = {} by A20;

        hence thesis by A3, FVSUM_1: 4;

      end;

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

      then P[( card X)];

      hence thesis by A2;

    end;

    reserve s for Element of ( 2Set ( Seg (n + 2)));

    theorem :: MATRIX11:5

    

     Th5: (( Part_sgn (p2,K)) . s) = ( 1_ K) or (( Part_sgn (p2,K)) . s) = ( - ( 1_ K))

    proof

      consider i, j such that

       A1: i in ( Seg (n + 2)) and

       A2: j in ( Seg (n + 2)) and

       A3: i < j and

       A4: s = {i, j} by Th1;

      p2 is Permutation of ( Seg (n + 2)) by MATRIX_1:def 12;

      then (p2 . i) <> (p2 . j) by A1, A2, A3, FUNCT_2: 19;

      then (p2 . i) > (p2 . j) or (p2 . i) < (p2 . j) by XXREAL_0: 1;

      hence thesis by A1, A2, A3, A4, Def1;

    end;

    theorem :: MATRIX11:6

    

     Th6: for i, j st i in ( Seg (n + 2)) & j in ( Seg (n + 2)) & i < j & (p2 . i) = (q2 . i) & (p2 . j) = (q2 . j) holds (( Part_sgn (p2,K)) . {i, j}) = (( Part_sgn (q2,K)) . {i, j})

    proof

      set n2 = (n + 2);

      let i, j such that

       A1: i in ( Seg n2) and

       A2: j in ( Seg n2) and

       A3: i < j and

       A4: (p2 . i) = (q2 . i) and

       A5: (p2 . j) = (q2 . j);

      reconsider p29 = p2 as Permutation of ( Seg n2) by MATRIX_1:def 12;

      

       A6: (p29 . i) <> (p29 . j) by A1, A2, A3, FUNCT_2: 19;

      now

        per cases by A6, XXREAL_0: 1;

          suppose

           A7: (p2 . i) < (p2 . j);

          then (( Part_sgn (p2,K)) . {i, j}) = ( 1_ K) by A1, A2, A3, Def1;

          hence thesis by A1, A2, A3, A4, A5, A7, Def1;

        end;

          suppose

           A8: (p2 . i) > (p2 . j);

          then (( Part_sgn (p2,K)) . {i, j}) = ( - ( 1_ K)) by A1, A2, A3, Def1;

          hence thesis by A1, A2, A3, A4, A5, A8, Def1;

        end;

      end;

      hence thesis;

    end;

    theorem :: MATRIX11:7

    

     Th7: for X be Element of ( Fin ( 2Set ( Seg (n + 2)))), p2, q2 holds for F be finite set st F = { s : s in X & (( Part_sgn (p2,K)) . s) <> (( Part_sgn (q2,K)) . s) } holds ((( card F) mod 2) = 0 implies (the multF of K $$ (X,( Part_sgn (p2,K)))) = (the multF of K $$ (X,( Part_sgn (q2,K))))) & ((( card F) mod 2) = 1 implies (the multF of K $$ (X,( Part_sgn (p2,K)))) = ( - (the multF of K $$ (X,( Part_sgn (q2,K))))))

    proof

      let X be Element of ( Fin ( 2Set ( Seg (n + 2))));

      let p2, q2;

      let F be finite set such that

       A1: F = { s : s in X & (( Part_sgn (p2,K)) . s) <> (( Part_sgn (q2,K)) . s) };

      set Pq = ( Part_sgn (q2,K));

      set Pp = ( Part_sgn (p2,K));

      set 2S = ( 2Set ( Seg (n + 2)));

      X c= 2S by FINSUB_1:def 5;

      then (X \ F) c= 2S;

      then

      reconsider Y = (X \ F) as Element of ( Fin 2S) by FINSUB_1:def 5;

      

       A2: F c= X

      proof

        let x be object;

        assume x in F;

        then ex s st x = s & s in X & (Pp . s) <> (Pq . s) by A1;

        hence thesis;

      end;

      then

       A3: (F \/ Y) = X by XBOOLE_1: 45;

      X c= 2S by FINSUB_1:def 5;

      then F c= 2S by A2;

      then

      reconsider F9 = F as Element of ( Fin 2S) by FINSUB_1:def 5;

      set KK = the carrier of K;

      set mm = the multF of K;

      consider Gp be Function of ( Fin 2S), KK such that

       A4: (mm $$ (F9,Pp)) = (Gp . F) and

       A5: for e be Element of KK st e is_a_unity_wrt mm holds (Gp . {} ) = e and

       A6: for x be Element of 2S holds (Gp . {x}) = (Pp . x) and

       A7: for B be Element of ( Fin 2S) st B c= F & B <> {} holds for x be Element of 2S st x in (F9 \ B) holds (Gp . (B \/ {x})) = (mm . ((Gp . B),(Pp . x))) by SETWISEO:def 3;

      

       A8: Y c= 2S by FINSUB_1:def 5;

      consider Gq be Function of ( Fin 2S), KK such that

       A9: (mm $$ (F9,Pq)) = (Gq . F) and

       A10: for e be Element of KK st e is_a_unity_wrt mm holds (Gq . {} ) = e and

       A11: for x be Element of 2S holds (Gq . {x}) = (Pq . x) and

       A12: for B be Element of ( Fin 2S) st B c= F & B <> {} holds for x be Element of 2S st x in (F \ B) holds (Gq . (B \/ {x})) = (mm . ((Gq . B),(Pq . x))) by SETWISEO:def 3;

      defpred P[ Nat] means for B be Element of ( Fin 2S) st ( card B) = $1 & B c= F holds ((( card B) mod 2) = 0 implies (Gp . B) = (Gq . B)) & ((( card B) mod 2) = 1 implies (Gp . B) = ( - (Gq . B)));

      

       A13: for s st s in F holds (Pp . s) = ( - (Pq . s))

      proof

        let s;

        assume s in F;

        then

         A14: ex s9 be Element of 2S st s9 = s & s9 in X & (Pp . s9) <> (Pq . s9) by A1;

        

         A15: (Pq . s) = ( 1_ K) or (Pq . s) = ( - ( 1_ K)) by Th5;

        (Pp . s) = ( 1_ K) or (Pp . s) = ( - ( 1_ K)) by Th5;

        then ((Pp . s) + (Pq . s)) = ( 0. K) by A14, A15, RLVECT_1:def 10;

        hence thesis by VECTSP_1: 16;

      end;

      

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

      proof

        let k be Nat such that

         A17: P[k];

        set k1 = (k + 1);

        let B be Element of ( Fin 2S) such that

         A18: ( card B) = k1 and

         A19: B c= F;

        now

          per cases ;

            case

             A20: k = 0 ;

            then

            consider x be object such that

             A21: B = {x} by A18, CARD_2: 42;

            

             A22: x in B by A21, TARSKI:def 1;

            B c= 2S by FINSUB_1:def 5;

            then

            reconsider x as Element of 2S by A22;

            

             A23: (Gq . B) = (Pq . x) by A11, A21;

            (Gp . B) = (Pp . x) by A6, A21;

            hence thesis by A13, A18, A19, A20, A22, A23, NAT_D: 14;

          end;

            case

             A24: k > 0 ;

            consider x be object such that

             A25: x in B by A18, CARD_1: 27, XBOOLE_0:def 1;

            B c= 2S by FINSUB_1:def 5;

            then

            reconsider x as Element of 2S by A25;

            B c= 2S by FINSUB_1:def 5;

            then (B \ {x}) c= 2S;

            then

            reconsider B9 = (B \ {x}) as Element of ( Fin 2S) by FINSUB_1:def 5;

            

             A26: not x in B9 by ZFMISC_1: 56;

            then

             A27: x in (F \ B9) by A19, A25, XBOOLE_0:def 5;

            

             A28: B9 c= F by A19;

            

             A29: ( {x} \/ B9) = B by A25, ZFMISC_1: 116;

            then

             A30: (k + 1) = (( card B9) + 1) by A18, A26, CARD_2: 41;

            then

             A31: (Gq . B) = (mm . ((Gq . B9),(Pq . x))) by A12, A19, A24, A29, A27, CARD_1: 27, XBOOLE_1: 1;

            

             A32: (Gp . B) = (mm . ((Gp . B9),(Pp . x))) by A7, A19, A24, A29, A30, A27, CARD_1: 27, XBOOLE_1: 1;

            now

              per cases by NAT_D: 12;

                case

                 A33: (k mod 2) = 0 ;

                 0 < (2 - 1);

                then

                 A34: (k1 mod 2) = ( 0 + 1) by A33, NAT_D: 70;

                

                 A35: (Gp . B) = ((Gp . B9) * ( - (Pq . x))) by A13, A19, A25, A32;

                (Gq . B) = ((Gp . B9) * (Pq . x)) by A17, A30, A28, A31, A33;

                hence thesis by A18, A35, A34, VECTSP_1: 8;

              end;

                case

                 A36: (k mod 2) = 1;

                

                 A37: (Pp . x) = ( - (Pq . x)) by A13, A19, A25;

                (Gp . B9) = ( - (Gq . B9)) by A17, A30, A28, A36;

                then

                 A38: (Gp . B) = (( - (Gq . B9)) * ( - (Pq . x))) by A7, A19, A24, A29, A30, A27, A37, CARD_1: 27, XBOOLE_1: 1;

                

                 A39: (2 - 1) = 1;

                (Gq . B) = ((Gq . B9) * (Pq . x)) by A12, A19, A24, A29, A30, A27, CARD_1: 27, XBOOLE_1: 1;

                hence thesis by A18, A36, A38, A39, NAT_D: 69, VECTSP_1: 10;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A40: P[ 0 ]

      proof

        let B be Element of ( Fin 2S) such that

         A41: ( card B) = 0 and B c= F;

        

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

        

         A43: B = {} by A41;

        then (Gp . B) = ( 1_ K) by A5, FVSUM_1: 4;

        hence thesis by A10, A43, A42, FVSUM_1: 4;

      end;

      

       A44: for k be Nat holds P[k] from NAT_1:sch 2( A40, A16);

      

       A45: Y misses F by XBOOLE_1: 79;

      then

       A46: (mm $$ (X,Pp)) = (mm . ((mm $$ (Y,Pp)),(mm $$ (F9,Pp)))) by A3, SETWOP_2: 4;

      

       A47: (mm $$ (X,Pq)) = (mm . ((mm $$ (Y,Pq)),(mm $$ (F9,Pq)))) by A45, A3, SETWOP_2: 4;

      

       A48: ( dom Pp) = 2S by FUNCT_2:def 1;

      then

       A49: ( dom (Pp | Y)) = Y by A8, RELAT_1: 62;

      ( dom Pq) = 2S by FUNCT_2:def 1;

      then

       A50: ( dom (Pq | Y)) = Y by A8, RELAT_1: 62;

      for x be object st x in ( dom (Pp | Y)) holds ((Pp | Y) . x) = ((Pq | Y) . x)

      proof

        let x be object such that

         A51: x in ( dom (Pp | Y));

        Y c= 2S by FINSUB_1:def 5;

        then

        reconsider x9 = x as Element of 2S by A49, A51;

        

         A52: ((Pp | Y) . x9) = (Pp . x9) by A51, FUNCT_1: 47;

        

         A53: not x9 in F by A49, A51, XBOOLE_0:def 5;

        assume

         A54: ((Pp | Y) . x) <> ((Pq | Y) . x);

        ((Pq | Y) . x9) = (Pq . x9) by A49, A50, A51, FUNCT_1: 47;

        hence contradiction by A1, A49, A51, A54, A52, A53;

      end;

      then

       A55: (Pp | Y) = (Pq | Y) by A48, A8, A50, FUNCT_1: 2, RELAT_1: 62;

      then

       A56: (mm $$ (Y,Pp)) = (mm $$ (Y,Pq)) by SETWOP_2: 7;

      now

        per cases by NAT_D: 12;

          case (( card F) mod 2) = 0 ;

          hence thesis by A4, A9, A44, A56, A46, A47;

        end;

          case

           A57: (( card F) mod 2) = 1;

          

           A58: (mm $$ (X,Pq)) = ((mm $$ (Y,Pp)) * (mm $$ (F9,Pq))) by A55, A47, SETWOP_2: 7;

          (mm $$ (X,Pp)) = ((mm $$ (Y,Pp)) * ( - (mm $$ (F9,Pq)))) by A4, A9, A44, A46, A57;

          hence thesis by A57, A58, VECTSP_1: 8;

        end;

      end;

      hence thesis;

    end;

    theorem :: MATRIX11:8

    

     Th8: for P be Permutation of ( Seg n) st P is being_transposition holds for i, j st i < j holds (P . i) = j iff i in ( dom P) & j in ( dom P) & (P . i) = j & (P . j) = i & for k st k <> i & k <> j & k in ( dom P) holds (P . k) = k

    proof

      let P;

      assume P is being_transposition;

      then

      consider i9,j9 be Nat such that i9 in ( dom P) and j9 in ( dom P) and i9 <> j9 and

       A1: (P . i9) = j9 and

       A2: (P . j9) = i9 and

       A3: for k st k <> i9 & k <> j9 & k in ( dom P) holds (P . k) = k;

      let i, j such that

       A4: i < j;

      thus (P . i) = j implies (i in ( dom P) & j in ( dom P) & (P . i) = j & (P . j) = i & for k st k <> i & k <> j & k in ( dom P) holds (P . k) = k)

      proof

        

         A5: ( dom P) = ( Seg n) by FUNCT_2: 52;

        

         A6: ( rng P) = ( Seg n) by FUNCT_2:def 3;

        assume

         A7: (P . i) = j;

        then

         A8: i in ( dom P) by A4, FUNCT_1:def 2;

        then i = j9 or i = i9 by A4, A3, A7;

        hence thesis by A1, A2, A3, A7, A8, A6, A5, FUNCT_1:def 3;

      end;

      thus thesis;

    end;

    theorem :: MATRIX11:9

    

     Th9: for p2, q2, pq2, i, j st pq2 = (p2 * q2) & q2 is being_transposition & (q2 . i) = j & i < j holds for s st (( Part_sgn (p2,K)) . s) <> (( Part_sgn (pq2,K)) . s) holds i in s or j in s

    proof

      set n2 = (n + 2);

      let p,q,pq be Element of ( Permutations n2), i, j such that

       A1: pq = (p * q) and

       A2: q is being_transposition and

       A3: (q . i) = j and

       A4: i < j;

      reconsider q9 = q, pq9 = pq as Permutation of ( Seg n2) by MATRIX_1:def 12;

      let s be Element of ( 2Set ( Seg n2)) such that

       A5: (( Part_sgn (p,K)) . s) <> (( Part_sgn (pq,K)) . s);

      

       A6: ( dom q9) = ( Seg n2) by FUNCT_2: 52;

      

       A7: ( dom pq9) = ( Seg n2) by FUNCT_2: 52;

      assume that

       A8: not i in s and

       A9: not j in s;

      consider i9,j9 be Nat such that

       A10: i9 in ( Seg n2) and

       A11: j9 in ( Seg n2) and

       A12: i9 < j9 and

       A13: s = {i9, j9} by Th1;

      

       A14: j <> j9 by A13, A9, TARSKI:def 2;

      

       A15: j <> i9 by A13, A9, TARSKI:def 2;

      i <> j9 by A13, A8, TARSKI:def 2;

      then (q . j9) = j9 by A2, A3, A4, A11, A14, A6, Th8;

      then

       A16: (pq . j9) = (p . j9) by A1, A11, A7, FUNCT_1: 12;

      i <> i9 by A13, A8, TARSKI:def 2;

      then (q . i9) = i9 by A2, A3, A4, A10, A15, A6, Th8;

      then (pq . i9) = (p . i9) by A1, A10, A7, FUNCT_1: 12;

      hence contradiction by A5, A10, A11, A12, A13, A16, Th6;

    end;

    

     Lm1: for i, j st i in ( Seg (n + 2)) & j in ( Seg (n + 2)) & i < j & ( 1_ K) <> ( - ( 1_ K)) holds ((( Part_sgn (p2,K)) . {i, j}) = ( 1_ K) implies (p2 . i) < (p2 . j)) & ((( Part_sgn (p2,K)) . {i, j}) = ( - ( 1_ K)) implies (p2 . i) > (p2 . j))

    proof

      set n2 = (n + 2);

      let i, j such that

       A1: i in ( Seg n2) and

       A2: j in ( Seg n2) and

       A3: i < j and

       A4: ( 1_ K) <> ( - ( 1_ K));

      reconsider p9 = p2 as Permutation of ( Seg n2) by MATRIX_1:def 12;

      (p9 . i) <> (p9 . j) by A1, A2, A3, FUNCT_2: 19;

      then

       A5: (p2 . i) < (p2 . j) or (p2 . i) > (p2 . j) by XXREAL_0: 1;

      thus (( Part_sgn (p2,K)) . {i, j}) = ( 1_ K) implies (p2 . i) < (p2 . j)

      proof

        (p9 . i) <> (p9 . j) by A1, A2, A3, FUNCT_2: 19;

        then

         A6: (p2 . i) < (p2 . j) or (p2 . i) > (p2 . j) by XXREAL_0: 1;

        assume (( Part_sgn (p2,K)) . {i, j}) = ( 1_ K);

        hence thesis by A1, A2, A3, A4, A6, Def1;

      end;

      assume (( Part_sgn (p2,K)) . {i, j}) = ( - ( 1_ K));

      hence thesis by A1, A2, A3, A4, A5, Def1;

    end;

    theorem :: MATRIX11:10

    

     Th10: for p2, q2, pq2, i, j, K st pq2 = (p2 * q2) & q2 is being_transposition & (q2 . i) = j & i < j & ( 1_ K) <> ( - ( 1_ K)) holds (( Part_sgn (p2,K)) . {i, j}) <> (( Part_sgn (pq2,K)) . {i, j}) & for k st k in ( Seg (n + 2)) & i <> k & j <> k holds (( Part_sgn (p2,K)) . {i, k}) <> (( Part_sgn (pq2,K)) . {i, k}) iff (( Part_sgn (p2,K)) . {j, k}) <> (( Part_sgn (pq2,K)) . {j, k})

    proof

      set n2 = (n + 2);

      let p,q,pq be Element of ( Permutations n2), i, j, K such that

       A1: pq = (p * q) and

       A2: q is being_transposition and

       A3: (q . i) = j and

       A4: i < j and

       A5: ( 1_ K) <> ( - ( 1_ K));

      

       A6: i in ( dom q) by A2, A3, A4, Th8;

      set P2 = ( Part_sgn (pq,K));

      set P1 = ( Part_sgn (p,K));

      reconsider p9 = p, q9 = q, pq9 = pq as Permutation of ( Seg n2) by MATRIX_1:def 12;

      

       A7: ( dom q9) = ( Seg n2) by FUNCT_2: 52;

      

       A8: j in ( dom q) by A2, A3, A4, Th8;

      

       A9: ( dom pq9) = ( Seg n2) by FUNCT_2: 52;

      then

       A10: (pq . i) = (p . j) by A1, A3, A6, A7, FUNCT_1: 12;

      (q . j) = i by A2, A3, A4, Th8;

      then

       A11: (pq . j) = (p . i) by A1, A8, A9, A7, FUNCT_1: 12;

      ( dom p9) = ( Seg n2) by FUNCT_2: 52;

      then

       A12: (p9 . i) <> (p9 . j) by A4, A6, A8, A7, FUNCT_1:def 4;

      now

        per cases by A12, XXREAL_0: 1;

          suppose

           A13: (p . i) < (p . j);

          then (P1 . {i, j}) = ( 1_ K) by A4, A6, A8, A7, Def1;

          hence (P1 . {i, j}) <> (P2 . {i, j}) by A4, A5, A6, A8, A7, A10, A11, A13, Def1;

        end;

          suppose

           A14: (p . i) > (p . j);

          then (P1 . {i, j}) = ( - ( 1_ K)) by A4, A6, A8, A7, Def1;

          hence (P1 . {i, j}) <> (P2 . {i, j}) by A4, A5, A6, A8, A7, A10, A11, A14, Def1;

        end;

      end;

      hence (P1 . {i, j}) <> (P2 . {i, j});

      let k such that

       A15: k in ( Seg n2) and

       A16: i <> k and

       A17: j <> k;

      

       A18: (q . k) = k by A2, A3, A4, A7, A15, A16, A17, Th8;

      

       A19: (pq . k) = (p . (q . k)) by A1, A9, A15, FUNCT_1: 12;

      i < k or k < i by A16, XXREAL_0: 1;

      then

       A20: {i, k} in ( 2Set ( Seg n2)) by A6, A7, A15, Th1;

      

       A21: (P1 . {i, k}) = (P2 . {i, k}) implies (P1 . {j, k}) = (P2 . {j, k})

      proof

        

         A22: j < k or k < j by A17, XXREAL_0: 1;

        

         A23: i < k or i > k by A16, XXREAL_0: 1;

        assume

         A24: (P1 . {i, k}) = (P2 . {i, k});

        (P1 . {k, i}) = ( 1_ K) or (P1 . {k, i}) = ( - ( 1_ K)) by A20, Th5;

        then (pq . j) < (pq . k) & (p . j) < (p . k) or (pq . j) > (pq . k) & (p . j) > (p . k) by A5, A6, A7, A10, A11, A15, A18, A19, A24, A23, Lm1;

        then (P2 . {j, k}) = ( 1_ K) & (P1 . {j, k}) = ( 1_ K) or (P2 . {j, k}) = ( - ( 1_ K)) & (P1 . {j, k}) = ( - ( 1_ K)) by A8, A7, A15, A22, Def1;

        hence thesis;

      end;

      j < k or k < j by A17, XXREAL_0: 1;

      then

       A25: {j, k} in ( 2Set ( Seg n2)) by A8, A7, A15, Th1;

      (P1 . {j, k}) = (P2 . {j, k}) implies (P1 . {i, k}) = (P2 . {i, k})

      proof

        

         A26: i < k or k < i by A16, XXREAL_0: 1;

        

         A27: j < k or j > k by A17, XXREAL_0: 1;

        assume

         A28: (P1 . {j, k}) = (P2 . {j, k});

        (P1 . {k, j}) = ( 1_ K) or (P1 . {k, j}) = ( - ( 1_ K)) by A25, Th5;

        then (pq . i) < (pq . k) & (p . i) < (p . k) or (pq . i) > (pq . k) & (p . i) > (p . k) by A5, A8, A7, A10, A11, A15, A18, A19, A28, A27, Lm1;

        then (P2 . {i, k}) = ( 1_ K) & (P1 . {i, k}) = ( 1_ K) or (P2 . {i, k}) = ( - ( 1_ K)) & (P1 . {i, k}) = ( - ( 1_ K)) by A6, A7, A15, A26, Def1;

        hence thesis;

      end;

      hence thesis by A21;

    end;

    definition

      let n, K;

      let perm2 be Element of ( Permutations (n + 2));

      :: MATRIX11:def2

      func sgn (perm2,K) -> Element of K equals (the multF of K $$ (( In (( 2Set ( Seg (n + 2))),( Fin ( 2Set ( Seg (n + 2)))))),( Part_sgn (perm2,K))));

      coherence ;

    end

    theorem :: MATRIX11:11

    

     Th11: ( sgn (p2,K)) = ( 1_ K) or ( sgn (p2,K)) = ( - ( 1_ K))

    proof

      set KK = the carrier of K;

      set n2 = (n + 2);

      set 2S = ( 2Set ( Seg n2));

      set mm = the multF of K;

      set Path = ( Part_sgn (p2,K));

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

      then ( In (2S,( Fin 2S))) = 2S by SUBSET_1:def 8;

      then

      reconsider 2S9 = 2S as Element of ( Fin 2S);

      consider G be Function of ( Fin 2S), KK such that

       A2: (mm $$ (2S9,Path)) = (G . 2S9) and

       A3: for e be Element of KK st e is_a_unity_wrt mm holds (G . {} ) = e and

       A4: for s holds (G . {s}) = (Path . s) and

       A5: for B be Element of ( Fin 2S) st B c= 2S9 & B <> {} holds for s st s in (2S9 \ B) holds (G . (B \/ {s})) = (mm . ((G . B),(Path . s))) by SETWISEO:def 3;

      defpred P[ Nat] means for B be Element of ( Fin 2S) st ( card B) = $1 & B c= 2S holds ((G . B) = ( 1_ K) or (G . B) = ( - ( 1_ K)));

      

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

      proof

        let k be Nat such that

         A7: P[k];

        set k1 = (k + 1);

        let B be Element of ( Fin 2S) such that

         A8: ( card B) = k1 and

         A9: B c= 2S;

        now

          per cases ;

            case k = 0 ;

            then

            consider x be object such that

             A10: B = {x} by A8, CARD_2: 42;

            x in B by A10, TARSKI:def 1;

            then

            reconsider x as Element of 2S by A9;

            (G . B) = (Path . x) by A4, A10;

            hence thesis by Th5;

          end;

            case

             A11: k > 0 ;

            consider x be object such that

             A12: x in B by A8, CARD_1: 27, XBOOLE_0:def 1;

            reconsider x as Element of 2S by A9, A12;

            (B \ {x}) c= 2S by A9;

            then

            reconsider B9 = (B \ {x}) as Element of ( Fin 2S) by FINSUB_1:def 5;

            

             A13: not x in B9 by ZFMISC_1: 56;

            

             A14: ( {x} \/ B9) = B by A12, ZFMISC_1: 116;

            then

             A15: (k + 1) = (( card B9) + 1) by A8, A13, CARD_2: 41;

            then

             A16: (G . B9) = ( 1_ K) or (G . B9) = ( - ( 1_ K)) by A7, A9, XBOOLE_1: 1;

            x in (2S \ B9) by A13, XBOOLE_0:def 5;

            then (G . B) = (mm . ((G . B9),(Path . x))) by A5, A9, A11, A14, A15, CARD_1: 27, XBOOLE_1: 1;

            then (G . B) = (( 1_ K) * ( 1_ K)) or (G . B) = (( 1_ K) * ( - ( 1_ K))) or (G . B) = (( - ( 1_ K)) * ( 1_ K)) or (G . B) = (( - ( 1_ K)) * ( - ( 1_ K))) by A16, Th5;

            then (G . B) = (( 1_ K) * ( 1_ K)) or (G . B) = (( 1_ K) * ( - ( 1_ K))) by VECTSP_1: 10;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A17: P[ 0 ]

      proof

        let B be Element of ( Fin 2S) such that

         A18: ( card B) = 0 and B c= 2S;

        B = {} by A18;

        hence thesis by A3, FVSUM_1: 4;

      end;

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

      then P[( card 2S9)];

      hence thesis by A2;

    end;

    theorem :: MATRIX11:12

    

     Th12: for Id be Element of ( Permutations (n + 2)) st Id = ( idseq (n + 2)) holds ( sgn (Id,K)) = ( 1_ K)

    proof

      set n2 = (n + 2);

      let Id be Element of ( Permutations n2) such that

       A1: Id = ( idseq n2);

      set Path = ( Part_sgn (Id,K));

      set 2S = ( 2Set ( Seg n2));

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

      then ( In (2S,( Fin 2S))) = 2S by SUBSET_1:def 8;

      then

      reconsider 2S9 = 2S as Element of ( Fin 2S);

      now

        let x;

        assume x in 2S9;

        then

        consider i, j such that

         A3: i in ( Seg n2) and

         A4: j in ( Seg n2) and

         A5: i < j and

         A6: x = {i, j} by Th1;

        

         A7: (Id . j) = j by A1, A4, FUNCT_1: 18;

        (Id . i) = i by A1, A3, FUNCT_1: 18;

        hence (Path . x) = ( 1_ K) by A3, A4, A5, A6, A7, Def1;

      end;

      hence thesis by Th4;

    end;

    

     Lm2: X in ( 2Set ( Seg n)) & i in X implies i in ( Seg n) & ex j st j in ( Seg n) & i <> j & X = {i, j}

    proof

      assume that

       A1: X in ( 2Set ( Seg n)) and

       A2: i in X;

      consider i9,j9 be Nat such that

       A3: i9 in ( Seg n) and

       A4: j9 in ( Seg n) and

       A5: i9 < j9 and

       A6: X = {i9, j9} by A1, Th1;

      now

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

          case i = i9;

          hence thesis by A3, A4, A5, A6;

        end;

          case i = j9;

          hence thesis by A3, A4, A5, A6;

        end;

      end;

      hence thesis;

    end;

    theorem :: MATRIX11:13

    

     Th13: for p2, q2, pq2 st pq2 = (p2 * q2) & q2 is being_transposition holds ( sgn (pq2,K)) = ( - ( sgn (p2,K)))

    proof

      set n2 = (n + 2);

      set 2SS = ( 2Set ( Seg n2));

      let p,q,pq be Element of ( Permutations n2) such that

       A1: pq = (p * q) and

       A2: q is being_transposition;

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

      then ( In (2SS,( Fin 2SS))) = 2SS by SUBSET_1:def 8;

      then

      reconsider 2S = 2SS as Element of ( Fin 2SS);

      

       A4: for i, j st i < j & (q . i) = j holds ( sgn (pq,K)) = ( - ( sgn (p,K)))

      proof

        let i, j such that

         A5: i < j and

         A6: (q . i) = j;

        now

          per cases ;

            suppose

             A7: ( 1_ K) = ( - ( 1_ K));

            then ( sgn (pq,K)) = ( - ( 1_ K)) by Th11;

            hence thesis by A7, Th11;

          end;

            suppose

             A8: ( 1_ K) <> ( - ( 1_ K));

            set P2 = ( Part_sgn (p,K));

            set P1 = ( Part_sgn (pq,K));

            

             A9: (P1 . {i, j}) <> (P2 . {i, j}) by A1, A2, A5, A6, A8, Th10;

            defpred P[ object, object] means ex D1 be set st D1 = $1 & for k st k in D1 & k <> i holds (k <> j implies $2 = {j, k}) & (k = j implies $2 = {i, j});

            set D = { s : s in 2S & (( Part_sgn (pq,K)) . s) <> (( Part_sgn (p,K)) . s) };

            D c= 2S

            proof

              let x be object;

              assume x in D;

              then ex s st x = s & s in 2S & (P1 . s) <> (P2 . s);

              hence thesis;

            end;

            then

            reconsider D as finite set;

            set D1 = { s : s in 2S & (P1 . s) <> (P2 . s) & i in s };

            set D2 = { s : s in 2S & (P1 . s) <> (P2 . s) & j in s };

            

             A10: D1 c= D

            proof

              let x be object;

              assume x in D1;

              then ex s st x = s & s in 2S & (P1 . s) <> (P2 . s) & i in s;

              hence thesis;

            end;

            

             A11: D2 c= D

            proof

              let x be object;

              assume x in D2;

              then ex s st x = s & s in 2S & (P1 . s) <> (P2 . s) & j in s;

              hence thesis;

            end;

            then

            reconsider D1, D2 as finite set by A10;

            

             A12: j in ( dom q) by A2, A5, A6, Th8;

            

             A13: D c= (D1 \/ D2)

            proof

              let x be object;

              assume x in D;

              then

              consider s such that

               A14: x = s and s in 2S and

               A15: (P1 . s) <> (P2 . s);

              i in s or j in s by A1, A2, A5, A6, A15, Th9;

              then x in D1 or x in D2 by A14, A15;

              hence thesis by XBOOLE_0:def 3;

            end;

            (D1 \/ D2) c= D by A10, A11, XBOOLE_1: 8;

            then

             A16: (D1 \/ D2) = D by A13;

            

             A17: (D1 /\ D2) c= { {i, j}}

            proof

              let x be object;

              assume

               A18: x in (D1 /\ D2);

              then x in D1 by XBOOLE_0:def 4;

              then

               A19: ex s1 be Element of 2SS st x = s1 & s1 in 2S & (P1 . s1) <> (P2 . s1) & i in s1;

              then

              consider i9,j9 be Nat such that i9 in ( Seg n2) and j9 in ( Seg n2) and i9 < j9 and

               A20: {i9, j9} = x by Th1;

              x in D2 by A18, XBOOLE_0:def 4;

              then ex s2 be Element of 2SS st x = s2 & s2 in 2S & (P1 . s2) <> (P2 . s2) & j in s2;

              then

               A21: j = i9 or j = j9 by A20, TARSKI:def 2;

              i = i9 or i = j9 by A19, A20, TARSKI:def 2;

              hence thesis by A5, A20, A21, TARSKI:def 1;

            end;

            q is Permutation of ( Seg n2) by MATRIX_1:def 12;

            then

             A22: ( dom q) = ( Seg n2) by FUNCT_2: 52;

            

             A23: i in ( dom q) by A2, A5, A6, Th8;

            then

             A24: {i, j} in 2S by A5, A12, A22, Th1;

            

             A25: i in {i, j} by TARSKI:def 2;

            then {i, j} in D1 by A24, A9;

            then ( card D1) > 0 ;

            then

            reconsider c1 = (( card D1) - 1) as Nat by NAT_1: 20;

            

             A26: j in {i, j} by TARSKI:def 2;

            then

             A27: {i, j} in D2 by A24, A9;

            

             A28: for x be object st x in D1 holds ex y be object st y in D2 & P[x, y]

            proof

              let x be object;

              assume x in D1;

              then

              consider s such that

               A29: x = s and s in 2S and

               A30: (P1 . s) <> (P2 . s) and

               A31: i in s;

              consider j9 be Nat such that

               A32: j9 in ( Seg n2) and

               A33: j9 <> i and

               A34: s = {i, j9} by A31, Lm2;

              now

                per cases ;

                  suppose

                   A35: j9 = j;

                  take X = {i, j};

                  thus X in D2 by A26, A24, A9;

                  reconsider xx = x as set by TARSKI: 1;

                  take xx;

                  thus xx = x;

                  let k such that

                   A36: k in xx and k <> i;

                  thus (k <> j implies X = {j, k}) & (k = j implies X = {i, j}) by A29, A34, A35, A36, TARSKI:def 2;

                end;

                  suppose

                   A37: j9 <> j;

                  take X = {j, j9};

                  j < j9 or j > j9 by A37, XXREAL_0: 1;

                  then

                   A38: X in 2SS by A12, A22, A32, Th1;

                  

                   A39: j in X by TARSKI:def 2;

                  (P1 . X) <> (P2 . X) by A1, A2, A5, A6, A8, A30, A32, A33, A34, A37, Th10;

                  hence X in D2 by A39, A38;

                  reconsider xx = x as set by TARSKI: 1;

                  take xx;

                  thus xx = x;

                  let k such that

                   A40: k in xx and

                   A41: k <> i;

                  thus (k <> j implies X = {j, k}) & (k = j implies X = {i, j}) by A29, A34, A37, A40, A41, TARSKI:def 2;

                end;

              end;

              hence thesis;

            end;

            consider f be Function of D1, D2 such that

             A42: for x be object st x in D1 holds P[x, (f . x)] from FUNCT_2:sch 1( A28);

            

             A43: {i, j} in D2 by A26, A24, A9;

            then

             A44: ( dom f) = D1 by FUNCT_2:def 1;

            for y be object st y in D2 holds ex x be object st x in D1 & y = (f . x)

            proof

              let y be object;

              assume y in D2;

              then

              consider s such that

               A45: s = y and s in 2S and

               A46: (P1 . s) <> (P2 . s) and

               A47: j in s;

              consider i1 be Nat such that

               A48: i1 in ( Seg n2) and

               A49: i1 <> j and

               A50: s = {j, i1} by A47, Lm2;

              now

                per cases ;

                  suppose

                   A51: i1 = i;

                  

                   A52: {i, j} in D1 by A25, A24, A9;

                  then P[s, (f . s)] by A42, A50, A51;

                  then (f . s) = y by A5, A26, A45, A50, A51;

                  hence thesis by A50, A51, A52;

                end;

                  suppose

                   A53: i1 <> i;

                  then i < i1 or i > i1 by XXREAL_0: 1;

                  then

                   A54: {i, i1} in 2SS by A23, A22, A48, Th1;

                  

                   A55: i in {i, i1} by TARSKI:def 2;

                  (P1 . {i, i1}) <> (P2 . {i, i1}) by A1, A2, A5, A6, A8, A46, A48, A49, A50, A53, Th10;

                  then

                   A56: {i, i1} in D1 by A54, A55;

                  

                   A57: i1 in {i, i1} by TARSKI:def 2;

                   P[ {i, i1}, (f . {i, i1})] by A42, A56;

                  then (f . {i, i1}) = {j, i1} by A49, A53, A57;

                  hence thesis by A45, A50, A56;

                end;

              end;

              hence thesis;

            end;

            then

             A58: ( rng f) = D2 by FUNCT_2: 10;

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

            proof

              let x1,x2 be object such that

               A59: x1 in D1 and

               A60: x2 in D1 and

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

              consider s1 be Element of 2SS such that

               A62: x1 = s1 and s1 in 2S and (P1 . s1) <> (P2 . s1) and

               A63: i in s1 by A59;

              consider j1 be Nat such that j1 in ( Seg n2) and

               A64: i <> j1 and

               A65: {i, j1} = s1 by A63, Lm2;

              consider s2 be Element of 2SS such that

               A66: x2 = s2 and s2 in 2S and (P1 . s2) <> (P2 . s2) and

               A67: i in s2 by A60;

              consider j2 be Nat such that j2 in ( Seg n2) and

               A68: i <> j2 and

               A69: {i, j2} = s2 by A67, Lm2;

              

               A70: j2 in s2 by A69, TARSKI:def 2;

              

               A71: j1 in s1 by A65, TARSKI:def 2;

              now

                per cases ;

                  case j = j1 & j = j2;

                  hence thesis by A62, A65, A66, A69;

                end;

                  case

                   A72: j <> j1 & j = j2;

                   P[x2, (f . x2)] by A42, A60;

                  then

                   A73: (f . x2) = {i, j} by A66, A68, A70, A72;

                   P[x1, (f . x1)] by A42, A59;

                  then (f . x1) = {j, j1} by A62, A64, A71, A72;

                  hence thesis by A5, A61, A64, A67, A69, A72, A73, TARSKI:def 2;

                end;

                  case

                   A74: j = j1 & j <> j2;

                   P[x2, (f . x2)] by A42, A60;

                  then

                   A75: (f . x2) = {j, j2} by A66, A68, A70, A74;

                   P[x1, (f . x1)] by A42, A59;

                  then (f . x1) = {i, j} by A62, A64, A71, A74;

                  hence thesis by A5, A61, A63, A65, A68, A74, A75, TARSKI:def 2;

                end;

                  case

                   A76: j <> j1 & j <> j2;

                   P[x2, (f . x2)] by A42, A60;

                  then

                   A77: (f . x2) = {j, j2} by A66, A68, A70, A76;

                  

                   A78: j1 in {j, j1} by TARSKI:def 2;

                   P[x1, (f . x1)] by A42, A59;

                  then (f . x1) = {j, j1} by A62, A64, A71, A76;

                  hence thesis by A61, A62, A65, A66, A69, A76, A77, A78, TARSKI:def 2;

                end;

              end;

              hence thesis;

            end;

            then f is one-to-one by A43, FUNCT_2: 19;

            then (D1,D2) are_equipotent by A58, A44, WELLORD2:def 4;

            then

             A79: ( card D1) = ( card D2) by CARD_1: 5;

             {i, j} in D1 by A25, A24, A9;

            then {i, j} in (D1 /\ D2) by A27, XBOOLE_0:def 4;

            then { {i, j}} c= (D1 /\ D2) by ZFMISC_1: 31;

            then (D1 /\ D2) = { {i, j}} by A17;

            

            then ( card D) = ((( card D1) + ( card D1)) - ( card { {i, j}})) by A79, A16, CARD_2: 45

            .= (((c1 + 1) + (c1 + 1)) - 1) by CARD_1: 30

            .= ((2 * c1) + 1);

            then (( card D) mod 2) = (1 mod 2) by NAT_D: 21;

            hence thesis by Th7, NAT_D: 14;

          end;

        end;

        hence thesis;

      end;

      consider i, j such that i in ( dom q) and j in ( dom q) and

       A80: i <> j and

       A81: (q . i) = j and

       A82: (q . j) = i and for k st k <> i & k <> j & k in ( dom q) holds (q . k) = k by A2;

      i < j or j < i by A80, XXREAL_0: 1;

      hence thesis by A4, A81, A82;

    end;

    theorem :: MATRIX11:14

    

     Th14: for tr be Element of ( Permutations (n + 2)) st tr is being_transposition holds ( sgn (tr,K)) = ( - ( 1_ K))

    proof

      set n2 = (n + 2);

      set S = ( Seg n2);

      let tr be Element of ( Permutations n2) such that

       A1: tr is being_transposition;

      reconsider Tr = tr as Permutation of S by MATRIX_1:def 12;

      reconsider Id = ( idseq n2), IdTr = (( id S) * Tr) as Element of ( Permutations n2) by MATRIX_1:def 12;

      ( rng Tr) = S by FUNCT_2:def 3;

      then IdTr = Tr by RELAT_1: 54;

      then ( sgn (tr,K)) = ( - ( sgn (Id,K))) by A1, Th13;

      hence thesis by Th12;

    end;

    theorem :: MATRIX11:15

    

     Th15: for P be FinSequence of ( Group_of_Perm (n + 2)), p2 be Element of ( Permutations (n + 2)) st p2 = ( Product P) & (for i st i in ( dom P) holds ex trans be Element of ( Permutations (n + 2)) st (P . i) = trans & trans is being_transposition) holds ((( len P) mod 2) = 0 implies ( sgn (p2,K)) = ( 1_ K)) & ((( len P) mod 2) = 1 implies ( sgn (p2,K)) = ( - ( 1_ K)))

    proof

      set n2 = (n + 2);

      set G = ( Group_of_Perm n2);

      defpred P[ Nat] means for P be FinSequence of G, p2 st p2 = ( Product P) & ( len P) = $1 & (for i st i in ( dom P) holds ex trans be Element of ( Permutations n2) st (P . i) = trans & trans is being_transposition) holds ((( len P) mod 2) = 0 implies ( sgn (p2,K)) = ( 1_ K)) & ((( len P) mod 2) = 1 implies ( sgn (p2,K)) = ( - ( 1_ K)));

      

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

      proof

        let k be Nat such that

         A2: P[k];

        set k1 = (k + 1);

        let P be FinSequence of G, p2 such that

         A3: p2 = ( Product P) and

         A4: ( len P) = k1 and

         A5: for i st i in ( dom P) holds ex trans be Element of ( Permutations n2) st (P . i) = trans & trans is being_transposition;

        consider x be object, Q be FinSequence such that

         A6: P = ( <*x*> ^ Q) and

         A7: ( len P) = (( len Q) + 1) by A4, RELAT_1: 38, REWRITE1: 5;

        reconsider X = <*x*>, Q as FinSequence of G by A6, FINSEQ_1: 36;

        

         A8: for i st i in ( dom Q) holds ex trans be Element of ( Permutations n2) st (Q . i) = trans & trans is being_transposition

        proof

          let i such that

           A9: i in ( dom Q);

          (Q . i) = (P . (( len X) + i)) by A6, A9, FINSEQ_1:def 7;

          hence thesis by A5, A6, A9, FINSEQ_1: 28;

        end;

        (1 + 0 ) <= k1 by XREAL_1: 7;

        then 1 in ( Seg k1);

        then

         A10: 1 in ( dom P) by A4, FINSEQ_1:def 3;

        (P . 1) = x by A6, FINSEQ_1: 41;

        then

        consider tr be Element of ( Permutations n2) such that

         A11: x = tr and

         A12: tr is being_transposition by A5, A10;

        reconsider PQ = ( Product Q) as Element of ( Permutations n2) by MATRIX_1:def 13;

        reconsider Tr = tr as Element of G by MATRIX_1:def 13;

        

         A13: p2 = (Tr * ( Product Q)) by A3, A6, A11, GROUP_4: 7

        .= (PQ * tr) by MATRIX_1:def 13;

        then

         A14: ( sgn (p2,K)) = ( - ( sgn (PQ,K))) by A12, Th13;

        now

          per cases by NAT_D: 12;

            suppose

             A15: (( len Q) mod 2) = 0 ;

             0 < (2 - 1);

            then

             A16: (( len P) mod 2) = ( 0 + 1) by A7, A15, NAT_D: 70;

            ( sgn (PQ,K)) = ( 1_ K) by A2, A4, A7, A8, A15;

            hence thesis by A12, A13, A16, Th13;

          end;

            suppose

             A17: (( len Q) mod 2) = 1;

            

             A18: (2 - 1) = 1;

            ( sgn (PQ,K)) = ( - ( 1_ K)) by A2, A4, A7, A8, A17;

            hence thesis by A7, A14, A17, A18, NAT_D: 69, RLVECT_1: 17;

          end;

        end;

        hence thesis;

      end;

      

       A19: P[ 0 ]

      proof

        let P be FinSequence of G, p2 such that

         A20: p2 = ( Product P) and

         A21: ( len P) = 0 and for i st i in ( dom P) holds ex trans be Element of ( Permutations n2) st (P . i) = trans & trans is being_transposition;

        P = ( <*> the carrier of G) by A21;

        then ( Product P) = ( 1_ G) by GROUP_4: 8;

        then ( Product P) = ( idseq n2) by MATRIX_1: 15;

        hence thesis by A20, A21, Th12, NAT_D: 26;

      end;

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

      hence thesis;

    end;

    theorem :: MATRIX11:16

    

     Th16: for i, j, n st i < j & i in ( Seg n) & j in ( Seg n) holds ex tr be Element of ( Permutations n) st tr is being_transposition & (tr . i) = j

    proof

      let i, j, n such that

       A1: i < j and

       A2: i in ( Seg n) and

       A3: j in ( Seg n);

      defpred P[ object, object] means for k st k in ( Seg n) & k = $1 holds (k = i implies $2 = j) & (k = j implies $2 = i) & (k <> i & k <> j implies $2 = k);

      

       A4: for x be object st x in ( Seg n) holds ex y be object st y in ( Seg n) & P[x, y]

      proof

        let x be object such that

         A5: x in ( Seg n);

        reconsider m = x as Nat by A5;

        now

          per cases ;

            suppose m = i;

            then P[x, j];

            hence thesis by A3;

          end;

            suppose m = j;

            then P[x, i];

            hence thesis by A2;

          end;

            suppose m <> i & m <> j;

            then P[x, x];

            hence thesis by A5;

          end;

        end;

        hence thesis;

      end;

      consider f be Function of ( Seg n), ( Seg n) such that

       A6: for x be object st x in ( Seg n) holds P[x, (f . x)] from FUNCT_2:sch 1( A4);

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

      proof

        let x1,x2 be object such that

         A7: x1 in ( Seg n) and

         A8: x2 in ( Seg n) and

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

        reconsider k1 = x1 as Nat by A7;

        x1 = i or x1 = j or x1 <> i & x1 <> j;

        then

         A10: x1 = i & (f . x1) = j or x1 = j & (f . x1) = i or x1 <> i & x1 <> j & (f . x1) = k1 by A6, A7;

        x2 = i or x2 = j or x2 <> i & x2 <> j;

        hence thesis by A6, A8, A9, A10;

      end;

      then

       A11: f is one-to-one by A2, FUNCT_2: 19;

      for y be object st y in ( Seg n) holds ex x be object st x in ( Seg n) & y = (f . x)

      proof

        let y be object such that

         A12: y in ( Seg n);

        reconsider k = y as Nat by A12;

        k = i & (f . j) = i or k = j & (f . i) = j or k <> i & k <> j & (f . k) = k by A2, A3, A6, A12;

        hence thesis by A2, A3, A12;

      end;

      then ( rng f) = ( Seg n) by FUNCT_2: 10;

      then f is onto by FUNCT_2:def 3;

      then

      reconsider P = f as Element of ( Permutations n) by A11, MATRIX_1:def 12;

      

       A13: (P . j) = i by A3, A6;

      ( dom P) = ( Seg n) by A2, FUNCT_2:def 1;

      then

       A14: for k st k <> i & k <> j & k in ( dom P) holds (P . k) = k by A6;

      take P;

      

       A15: i in ( dom P) by A2, FUNCT_2:def 1;

      

       A16: j in ( dom P) by A3, FUNCT_2:def 1;

      (P . i) = j by A2, A6;

      hence thesis by A1, A15, A16, A13, A14;

    end;

    theorem :: MATRIX11:17

    

     Th17: for p be Element of ( Permutations (k + 1)) st (p . (k + 1)) <> (k + 1) holds ex tr be Element of ( Permutations (k + 1)) st tr is being_transposition & (tr . (p . (k + 1))) = (k + 1) & ((tr * p) . (k + 1)) = (k + 1)

    proof

      set k1 = (k + 1);

      let p be Element of ( Permutations k1) such that

       A1: (p . k1) <> k1;

      reconsider p9 = p as Permutation of ( Seg k1) by MATRIX_1:def 12;

      

       A2: ( dom p9) = ( Seg k1) by FUNCT_2: 52;

      

       A3: ( rng p9) = ( Seg k1) by FUNCT_2:def 3;

      

       A4: k1 in ( Seg k1) by FINSEQ_1: 3;

      then

       A5: (p . k1) in ( Seg k1) by A2, A3, FUNCT_1:def 3;

      then (p . k1) <= k1 by FINSEQ_1: 1;

      then (p . k1) < k1 by A1, XXREAL_0: 1;

      then

      consider tr be Element of ( Permutations k1) such that

       A6: tr is being_transposition and

       A7: (tr . (p . k1)) = k1 by A4, A5, Th16;

      reconsider tr9 = tr as Permutation of ( Seg k1) by MATRIX_1:def 12;

      ( dom tr9) = ( Seg k1) by FUNCT_2: 52;

      then ( dom (tr * p)) = ( Seg k1) by A2, A3, RELAT_1: 27;

      then ((tr * p) . k1) = (tr . (p . k1)) by FINSEQ_1: 3, FUNCT_1: 12;

      hence thesis by A6, A7;

    end;

    theorem :: MATRIX11:18

    

     Th18: for X, x st not x in X holds for p1 be Permutation of (X \/ {x}) st (p1 . x) = x holds ex p be Permutation of X st (p1 | X) = p

    proof

      let X, x such that

       A1: not x in X;

      let p1 be Permutation of (X \/ {x}) such that

       A2: (p1 . x) = x;

      

       A3: X c= (X \/ {x}) by XBOOLE_1: 7;

      set pX = (p1 | X);

      

       A4: ( dom p1) = (X \/ {x}) by FUNCT_2: 52;

      then

       A5: ( dom pX) = X by RELAT_1: 62, XBOOLE_1: 7;

      

       A6: ( rng p1) = (X \/ {x}) by FUNCT_2:def 3;

      then

       A7: ( rng pX) c= (X \/ {x}) by RELAT_1: 70;

      

       A8: ( rng pX) c= X

      proof

        let y be object such that

         A9: y in ( rng pX);

        consider x9 be object such that

         A10: x9 in ( dom pX) and

         A11: (pX . x9) = y by A9, FUNCT_1:def 3;

        assume

         A12: not y in X;

        y in ( rng pX) by A10, A11, FUNCT_1:def 3;

        then y in {x} by A7, A12, XBOOLE_0:def 3;

        then

         A13: y = x by TARSKI:def 1;

        (pX . x9) = (p1 . x9) by A10, FUNCT_1: 47;

        hence thesis by A1, A2, A3, A4, A5, A7, A9, A10, A11, A13, FUNCT_1:def 4;

      end;

      X c= ( rng pX)

      proof

        let y be object such that

         A14: y in X;

        consider x9 be object such that

         A15: x9 in ( dom p1) and

         A16: (p1 . x9) = y by A3, A6, A14, FUNCT_1:def 3;

        

         A17: x9 in X

        proof

          assume not x9 in X;

          then x9 in {x} by A4, A15, XBOOLE_0:def 3;

          hence thesis by A1, A2, A14, A16, TARSKI:def 1;

        end;

        then (pX . x9) = (p1 . x9) by A5, FUNCT_1: 47;

        hence thesis by A5, A16, A17, FUNCT_1:def 3;

      end;

      then

       A18: ( rng pX) = X by A8;

      

       A19: pX is one-to-one by FUNCT_1: 52;

      reconsider pX as Function of X, X by A5, A18, FUNCT_2: 1;

      pX is onto by A18, FUNCT_2:def 3;

      hence thesis by A19;

    end;

    theorem :: MATRIX11:19

    

     Th19: for p,q be Permutation of X, p1,q1 be Permutation of (X \/ {x}) st (p1 | X) = p & (q1 | X) = q & (p1 . x) = x & (q1 . x) = x holds ((p1 * q1) | X) = (p * q) & ((p1 * q1) . x) = x

    proof

      let p,q be Permutation of X, p1,q1 be Permutation of (X \/ {x}) such that

       A1: (p1 | X) = p and

       A2: (q1 | X) = q and

       A3: (p1 . x) = x and

       A4: (q1 . x) = x;

      set pq = (p * q);

      set pq1 = (p1 * q1);

      set X1 = (X \/ {x});

      

       A5: X c= X1 by XBOOLE_1: 7;

      

       A6: ( rng q) = X by FUNCT_2:def 3;

      

       A7: ( dom q) = X by FUNCT_2: 52;

      ( dom pq1) = X1 by FUNCT_2: 52;

      then

       A8: ( dom (pq1 | X)) = X by RELAT_1: 62, XBOOLE_1: 7;

      

       A9: ( dom pq) = X by FUNCT_2: 52;

      

       A10: ( dom p) = X by FUNCT_2: 52;

      for y be object st y in ( dom pq) holds (pq . y) = ((pq1 | X) . y)

      proof

        let y be object such that

         A11: y in ( dom pq);

        

         A12: (pq . y) = (p . (q . y)) by A9, A11, FUNCT_2: 15;

        

         A13: (pq1 . y) = ((pq1 | X) . y) by A9, A8, A11, FUNCT_1: 47;

        

         A14: (q . y) in ( rng q) by A7, A9, A11, FUNCT_1:def 3;

        

         A15: (pq1 . y) = (p1 . (q1 . y)) by A5, A9, A11, FUNCT_2: 15;

        (q1 . y) = (q . y) by A2, A7, A9, A11, FUNCT_1: 47;

        hence thesis by A1, A10, A6, A14, A13, A12, A15, FUNCT_1: 47;

      end;

      hence (pq1 | X) = pq by A8, FUNCT_1: 2, FUNCT_2: 52;

      x in {x} by TARSKI:def 1;

      then x in X1 by XBOOLE_0:def 3;

      hence thesis by A3, A4, FUNCT_2: 15;

    end;

    theorem :: MATRIX11:20

    

     Th20: for tr be Element of ( Permutations k) st tr is being_transposition holds (tr * tr) = ( idseq k) & tr = (tr " )

    proof

      set I = ( idseq k);

      let tr be Element of ( Permutations k);

      assume tr is being_transposition;

      then

      consider i, j such that i in ( dom tr) and j in ( dom tr) and i <> j and

       A1: (tr . i) = j and

       A2: (tr . j) = i and

       A3: for m st m <> i & m <> j & m in ( dom tr) holds (tr . m) = m;

      reconsider TR = tr as Permutation of ( Seg k) by MATRIX_1:def 12;

      set TT = (TR * TR);

      

       A4: ( dom TT) = ( Seg k) by FUNCT_2: 52;

      

       A5: ( dom TR) = ( Seg k) by FUNCT_2: 52;

      

       A6: for x be object st x in ( dom TT) holds (TT . x) = (I . x)

      proof

        let x be object such that

         A7: x in ( dom TT);

        reconsider m = x as Nat by A4, A7;

        now

          per cases ;

            suppose m = i or m = j;

            hence (TT . m) = m by A1, A2, A7, FUNCT_1: 12;

          end;

            suppose m <> i & m <> j;

            then (tr . m) = m by A3, A4, A5, A7;

            hence (TT . m) = m by A7, FUNCT_1: 12;

          end;

        end;

        hence thesis by A4, A7, FUNCT_1: 18;

      end;

      

       A8: ( dom I) = ( Seg k);

      hence (tr * tr) = ( idseq k) by A6, FUNCT_1: 2, FUNCT_2: 52;

      ( rng TR) = ( Seg k) by FUNCT_2:def 3;

      hence thesis by A4, A8, A5, A6, FUNCT_1: 2, FUNCT_1: 42;

    end;

    theorem :: MATRIX11:21

    

     Th21: for perm holds ex P be FinSequence of ( Group_of_Perm n) st perm = ( Product P) & for i st i in ( dom P) holds ex trans be Element of ( Permutations n) st (P . i) = trans & trans is being_transposition

    proof

      defpred P[ Nat] means for perm be Element of ( Permutations $1) holds ex P be FinSequence of ( Group_of_Perm $1) st perm = ( Product P) & for i st i in ( dom P) holds ex trans be Element of ( Permutations $1) st (P . i) = trans & trans is being_transposition;

      let perm be Element of ( Permutations n);

      

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

      proof

        let k be Nat such that

         A2: P[k];

        set k1 = (k + 1);

        let p be Element of ( Permutations k1);

        reconsider p9 = p as Permutation of ( Seg k1) by MATRIX_1:def 12;

        set Gk1 = ( Group_of_Perm k1);

        

         A3: for p be Element of ( Permutations k1) st (p . k1) = k1 holds ex P be FinSequence of ( Group_of_Perm k1) st p = ( Product P) & for i st i in ( dom P) holds ex trans be Element of ( Permutations k1) st (P . i) = trans & trans is being_transposition

        proof

          set Ik = ( idseq k);

          set Ik1 = ( idseq k1);

          set Gk1 = ( Group_of_Perm k1);

          set Gk = ( Group_of_Perm k);

          let p be Element of ( Permutations k1) such that

           A4: (p . k1) = k1;

          set mG1 = the multF of Gk1;

          set mG = the multF of Gk;

          reconsider p9 = p as Permutation of ( Seg k1) by MATRIX_1:def 12;

          

           A5: ( Seg k1) = (( Seg k) \/ {k1}) by FINSEQ_1: 9;

          then

          consider pk be Permutation of ( Seg k) such that

           A6: (p9 | ( Seg k)) = pk by A4, Th18, FINSEQ_3: 8;

          reconsider pk9 = pk as Element of ( Permutations k) by MATRIX_1:def 12;

          consider P be FinSequence of Gk such that

           A7: pk9 = ( Product P) and

           A8: for i st i in ( dom P) holds ex trans be Element of ( Permutations k) st (P . i) = trans & trans is being_transposition by A2;

          

           A9: pk9 = (mG "**" P) by A7, GROUP_4:def 2;

          defpred PR[ set, set] means for i be Nat, tr be Element of ( Permutations k) st i in ( dom P) & (P . i) = tr & i = $1 holds ex newtr be Element of ( Permutations k1) st newtr = $2 & newtr is being_transposition & (newtr . k1) = k1 & tr = (newtr | ( Seg k));

          

           A10: not k1 in ( Seg k) by FINSEQ_3: 8;

          

           A11: for m be Nat st m in ( Seg ( len P)) holds ex x be Element of Gk1 st PR[m, x]

          proof

            let m be Nat;

            assume m in ( Seg ( len P));

            then m in ( dom P) by FINSEQ_1:def 3;

            then

            consider tr be Element of ( Permutations k) such that

             A12: (P . m) = tr and

             A13: tr is being_transposition by A8;

            consider i9,j9 be Nat such that

             A14: i9 in ( dom tr) and

             A15: j9 in ( dom tr) and

             A16: i9 <> j9 and

             A17: (tr . i9) = j9 and

             A18: (tr . j9) = i9 and

             A19: for k st k <> i9 & k <> j9 & k in ( dom tr) holds (tr . k) = k by A13;

            reconsider tr9 = tr as Permutation of ( Seg k) by MATRIX_1:def 12;

            consider newt be Function of ( Seg k1), ( Seg k1) such that

             A20: (newt | ( Seg k)) = tr9 and

             A21: (newt . k1) = k1 by A5, A10, STIRL2_1: 57;

            

             A22: (newt . j9) = (tr . j9) by A20, A15, FUNCT_1: 47;

            

             A23: ( Seg k) is empty implies ( Seg k) is empty;

            then

             A24: newt is onto by A5, A20, A21, STIRL2_1: 58;

            newt is one-to-one by A5, A10, A23, A20, A21, STIRL2_1: 58;

            then

            reconsider NT = newt as Element of ( Permutations k1) by A24, MATRIX_1:def 12;

            reconsider NT9 = NT as Element of Gk1 by MATRIX_1:def 13;

            take NT9;

            let I be Nat, TR be Element of ( Permutations k) such that I in ( dom P) and

             A25: (P . I) = TR and

             A26: I = m;

            take NT;

            

             A27: ( dom tr) c= ( dom newt) by A20, RELAT_1: 60;

            

             A28: for m st m <> i9 & m <> j9 & m in ( dom newt) holds (newt . m) = m

            proof

              

               A29: ( dom tr9) = ( Seg k) by FUNCT_2: 52;

              let m such that

               A30: m <> i9 and

               A31: m <> j9 and

               A32: m in ( dom newt);

              ( dom newt) = ( Seg k1) by FUNCT_2: 52;

              then m in ( Seg k) or m in {k1} by A5, A32, XBOOLE_0:def 3;

              then m in ( dom tr) or m = k1 by A29, TARSKI:def 1;

              then (tr . m) = (newt . m) & (tr . m) = m or (newt . m) = m by A20, A21, A19, A30, A31, FUNCT_1: 47;

              hence thesis;

            end;

            (newt . i9) = (tr . i9) by A20, A14, FUNCT_1: 47;

            hence thesis by A12, A20, A21, A25, A26, A14, A15, A16, A17, A18, A27, A22, A28;

          end;

          consider Pr be FinSequence of Gk1 such that

           A33: ( dom Pr) = ( Seg ( len P)) and

           A34: for m be Nat st m in ( Seg ( len P)) holds PR[m, (Pr . m)] from FINSEQ_1:sch 5( A11);

          take Pr;

          

           A35: ( Product Pr) = (mG1 "**" Pr) by GROUP_4:def 2;

          now

            per cases ;

              suppose

               A36: ( len Pr) = 0 ;

              then

               A37: ( Seg ( len Pr)) = 0 ;

              

               A38: ( Product Pr) = ( the_unity_wrt mG1) by A35, A36, FINSOP_1:def 1;

              ( the_unity_wrt mG1) = ( 1_ Gk1) by GROUP_1: 22;

              then

               A39: ( Product Pr) = Ik1 by A38, MATRIX_1: 15;

              ( len P) = 0 by A33, A36, FINSEQ_1:def 3;

              then

               A40: pk9 = ( the_unity_wrt mG) by A9, FINSOP_1:def 1;

              

               A41: ( dom p9) = ( Seg k1) by FUNCT_2: 52;

              

               A42: ( the_unity_wrt mG) = ( 1_ Gk) by GROUP_1: 22;

              

               A43: for y be object st y in ( dom p) holds (p . y) = (Ik1 . y)

              proof

                let y be object such that

                 A44: y in ( dom p);

                reconsider y9 = y as Nat by A41, A44;

                

                 A45: (Ik1 . y9) = y9 by A41, A44, FUNCT_1: 18;

                

                 A46: ( dom pk) = ( Seg k) by FUNCT_2: 52;

                y in ( Seg k) or y in {k1} by A5, A41, A44, XBOOLE_0:def 3;

                then (pk . y) = (p . y) & (Ik . y9) = y9 or (p . k1) = k1 & y = k1 by A4, A6, A46, FUNCT_1: 18, FUNCT_1: 47, TARSKI:def 1;

                hence thesis by A40, A42, A45, MATRIX_1: 15;

              end;

              ( dom Ik1) = ( Seg k1);

              hence thesis by A39, A41, A43, A37, FINSEQ_1:def 3, FUNCT_1: 2;

            end;

              suppose

               A47: ( len Pr) > 0 ;

              consider fPr be sequence of Gk1 such that

               A48: (fPr . 1) = (Pr . 1) and

               A49: for n be Nat st 0 <> n & n < ( len Pr) holds (fPr . (n + 1)) = (mG1 . ((fPr . n),(Pr . (n + 1)))) and

               A50: ( Product Pr) = (fPr . ( len Pr)) by A35, A47, FINSOP_1:def 1;

              ( len P) > 0 by A33, A47, FINSEQ_1:def 3;

              then

              consider fP be sequence of Gk such that

               A51: (fP . 1) = (P . 1) and

               A52: for n be Nat st 0 <> n & n < ( len P) holds (fP . (n + 1)) = (mG . ((fP . n),(P . (n + 1)))) and

               A53: pk = (fP . ( len P)) by A9, FINSOP_1:def 1;

              

               A54: ( len P) = ( len Pr) by A33, FINSEQ_1:def 3;

              defpred N[ Nat] means ($1 > 0 & $1 <= ( len P)) implies ex Prod1 be Element of ( Permutations k1), Prod be Element of ( Permutations k) st Prod1 = (fPr . $1) & (fP . $1) = Prod & (Prod1 | ( Seg k)) = Prod & (Prod1 . k1) = k1;

              

               A55: for m be Nat st N[m] holds N[(m + 1)]

              proof

                let m be Nat such that

                 A56: N[m];

                set m1 = (m + 1);

                assume that m1 > 0 and

                 A57: m1 <= ( len P);

                (m1 + 0 ) > 0 ;

                then m1 >= 1 by NAT_1: 19;

                then

                 A58: m1 in ( Seg ( len P)) by A57;

                

                 A59: ( dom P) = ( Seg ( len P)) by FINSEQ_1:def 3;

                then

                consider tr be Element of ( Permutations k) such that

                 A60: (P . m1) = tr and tr is being_transposition by A8, A58;

                consider tr1 be Element of ( Permutations k1) such that

                 A61: tr1 = (Pr . m1) and tr1 is being_transposition and

                 A62: (tr1 . k1) = k1 and

                 A63: tr = (tr1 | ( Seg k)) by A34, A58, A59, A60;

                now

                  per cases ;

                    suppose m = 0 ;

                    hence thesis by A51, A48, A60, A61, A62, A63;

                  end;

                    suppose

                     A64: m > 0 ;

                    

                     A65: (m + 0 ) < (m + 1) by XREAL_1: 6;

                    then

                    consider Q1 be Element of ( Permutations k1), Q be Element of ( Permutations k) such that

                     A66: Q1 = (fPr . m) and

                     A67: (fP . m) = Q and

                     A68: (Q1 | ( Seg k)) = Q and

                     A69: (Q1 . k1) = k1 by A56, A57, A64, XXREAL_0: 2;

                    reconsider Q, tr as Permutation of ( Seg k) by MATRIX_1:def 12;

                    reconsider trQ = (tr * Q) as Element of ( Permutations k) by MATRIX_1:def 12;

                    

                     A70: m < ( len P) by A57, A65, XXREAL_0: 2;

                    then

                     A71: (fP . m1) = (mG . (Q,tr)) by A52, A60, A64, A67;

                    then

                     A72: (fP . m1) = trQ by MATRIX_1:def 13;

                    reconsider Q1, tr1 as Permutation of ( Seg k1) by MATRIX_1:def 12;

                    reconsider trQ1 = (tr1 * Q1) as Element of ( Permutations k1) by MATRIX_1:def 12;

                    

                     A73: (trQ1 | ( Seg k)) = trQ by A5, A62, A63, A68, A69, Th19;

                    ( len P) = ( len Pr) by A33, FINSEQ_1:def 3;

                    then (fPr . m1) = (mG1 . (Q1,tr1)) by A49, A61, A64, A66, A70;

                    then

                     A74: (fPr . m1) = trQ1 by MATRIX_1:def 13;

                    (trQ1 . k1) = k1 by A5, A62, A63, A68, A69, A71, Th19;

                    hence thesis by A72, A74, A73;

                  end;

                end;

                hence thesis;

              end;

              

               A75: N[ 0 ];

              for m be Nat holds N[m] from NAT_1:sch 2( A75, A55);

              then

              consider Prod1 be Element of ( Permutations k1), Prod be Element of ( Permutations k) such that

               A76: Prod1 = (fPr . ( len P)) and

               A77: (fP . ( len P)) = Prod and

               A78: (Prod1 | ( Seg k)) = Prod and

               A79: (Prod1 . k1) = k1 by A47, A54;

              reconsider Prod1 as Permutation of ( Seg k1) by MATRIX_1:def 12;

              

               A80: ( dom p9) = ( Seg k1) by FUNCT_2: 52;

              

               A81: for y be object st y in ( dom p) holds (p . y) = (Prod1 . y)

              proof

                let y be object;

                assume y in ( dom p);

                then

                 A82: y in ( Seg k) or y in {k1} by A5, A80, XBOOLE_0:def 3;

                ( dom pk) = ( Seg k) by FUNCT_2: 52;

                then (Prod . y) = (p . y) & (Prod . y) = (Prod1 . y) or y = k1 & (p . k1) = (Prod1 . k1) by A4, A6, A53, A77, A78, A79, A82, FUNCT_1: 47, TARSKI:def 1;

                hence thesis;

              end;

              ( dom Prod1) = ( Seg k1) by FUNCT_2: 52;

              hence p = ( Product Pr) by A50, A54, A76, A80, A81, FUNCT_1: 2;

              thus for i st i in ( dom Pr) holds ex trans be Element of ( Permutations k1) st (Pr . i) = trans & trans is being_transposition

              proof

                

                 A83: ( Seg ( len P)) = ( dom P) by FINSEQ_1:def 3;

                let m such that

                 A84: m in ( dom Pr);

                consider t be Element of ( Permutations k) such that

                 A85: (P . m) = t and t is being_transposition by A8, A33, A84, A83;

                reconsider m9 = m as Element of NAT by ORDINAL1:def 12;

                ex T be Element of ( Permutations k1) st T = (Pr . m9) & T is being_transposition & (T . k1) = k1 & t = (T | ( Seg k)) by A33, A34, A84, A83, A85;

                hence thesis;

              end;

            end;

          end;

          hence thesis;

        end;

        now

          per cases ;

            suppose (p . k1) = k1;

            hence thesis by A3;

          end;

            suppose

             A86: (p . k1) <> k1;

            

             A87: ( rng p9) = ( Seg k1) by FUNCT_2:def 3;

            consider tr be Element of ( Permutations k1) such that

             A88: tr is being_transposition and (tr . (p . k1)) = k1 and

             A89: ((tr * p) . k1) = k1 by A86, Th17;

            reconsider tr9 = tr as Permutation of ( Seg k1) by MATRIX_1:def 12;

            reconsider trp = (tr9 * p9) as Element of ( Permutations k1) by MATRIX_1:def 12;

            consider P be FinSequence of Gk1 such that

             A90: trp = ( Product P) and

             A91: for i st i in ( dom P) holds ex trans be Element of ( Permutations k1) st (P . i) = trans & trans is being_transposition by A3, A89;

            reconsider TRP = trp as Element of Gk1 by MATRIX_1:def 13;

            reconsider T = tr as Element of Gk1 by MATRIX_1:def 13;

            take PT = (P ^ <*T*>);

            ( Product PT) = (TRP * T) by A90, GROUP_4: 6;

            

            hence ( Product PT) = (tr * (tr * p)) by MATRIX_1:def 13

            .= ((tr * tr) * p) by RELAT_1: 36

            .= (( idseq k1) * p) by A88, Th20

            .= p by A87, RELAT_1: 54;

            thus for m st m in ( dom PT) holds ex trans be Element of ( Permutations k1) st (PT . m) = trans & trans is being_transposition

            proof

              set L = ( len P);

              set L1 = (L + 1);

              

               A92: ( Seg L1) = (( Seg L) \/ {L1}) by FINSEQ_1: 9;

              ( len PT) = (( len P) + 1) by FINSEQ_2: 16;

              then

               A93: ( dom PT) = ( Seg L1) by FINSEQ_1:def 3;

              let m such that

               A94: m in ( dom PT);

              now

                per cases by A94, A93, A92, XBOOLE_0:def 3;

                  suppose m in ( Seg L);

                  then

                   A95: m in ( dom P) by FINSEQ_1:def 3;

                  then (PT . m) = (P . m) by FINSEQ_1:def 7;

                  hence thesis by A91, A95;

                end;

                  suppose m in {L1};

                  then m = L1 by TARSKI:def 1;

                  hence thesis by A88, FINSEQ_1: 42;

                end;

              end;

              hence thesis;

            end;

          end;

        end;

        hence thesis;

      end;

      

       A96: P[ 0 ]

      proof

        let perm be Element of ( Permutations 0 );

        take ( <*> the carrier of ( Group_of_Perm 0 ));

        perm is Permutation of ( Seg 0 ) by MATRIX_1:def 12;

        then perm = ( idseq 0 );

        then perm = ( 1_ ( Group_of_Perm 0 )) by MATRIX_1: 15;

        hence thesis by GROUP_4: 8;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A96, A1);

      hence thesis;

    end;

    

     th22: K is non degenerated well-unital & K is Fanoian implies ( 1_ K) <> ( - ( 1_ K))

    proof

      assume

       A0: K is non degenerated well-unital;

      assume

       A1: K is Fanoian;

      assume ( 1_ K) = ( - ( 1_ K));

      then (( 1_ K) + ( 1_ K)) = ( 0. K) by RLVECT_1:def 10;

      hence thesis by A0, A1;

    end;

    theorem :: MATRIX11:22

    

     Th22: K is non degenerated well-unital domRing-like implies (K is Fanoian iff ( 1_ K) <> ( - ( 1_ K)))

    proof

      assume

       A0: K is non degenerated well-unital domRing-like;

      thus K is Fanoian implies ( 1_ K) <> ( - ( 1_ K))

      proof

        assume

         A1: K is Fanoian;

        assume ( 1_ K) = ( - ( 1_ K));

        then (( 1_ K) + ( 1_ K)) = ( 0. K) by RLVECT_1:def 10;

        hence thesis by A0, A1;

      end;

      assume

       A2: ( 1_ K) <> ( - ( 1_ K));

      assume not K is Fanoian;

      then

      consider a be Element of K such that

       A3: (a + a) = ( 0. K) and

       A4: a <> ( 0. K);

      a = (a * ( 1_ K));

      then ( 0. K) = (a * (( 1_ K) + ( 1_ K))) by A3, VECTSP_1:def 7;

      then ( 0. K) = (( 1_ K) + ( 1_ K)) by A0, A4, VECTSP_2:def 1;

      hence thesis by A2, VECTSP_1: 16;

    end;

    theorem :: MATRIX11:23

    

     Th23: K is Fanoian non degenerated implies (perm2 is even iff ( sgn (perm2,K)) = ( 1_ K)) & (perm2 is odd iff ( sgn (perm2,K)) = ( - ( 1_ K)))

    proof

      assume

       A0: K is Fanoian non degenerated;

      set n2 = (n + 2);

      

       A1: ( len ( Permutations n2)) = n2 by MATRIX_1: 9;

      thus

       A2: perm2 is even implies ( sgn (perm2,K)) = ( 1_ K) by A1, Th15;

      thus ( sgn (perm2,K)) = ( 1_ K) implies perm2 is even

      proof

        assume

         A3: ( sgn (perm2,K)) = ( 1_ K);

        consider P be FinSequence of ( Group_of_Perm n2) such that

         A4: perm2 = ( Product P) and

         A5: for i st i in ( dom P) holds ex trans be Element of ( Permutations n2) st (P . i) = trans & trans is being_transposition by Th21;

        assume perm2 is odd;

        then (( len P) mod 2) <> 0 by A1, A4, A5;

        then (( len P) mod 2) = 1 by NAT_D: 12;

        then ( sgn (perm2,K)) = ( - ( 1_ K)) by A4, A5, Th15;

        hence thesis by A0, A3, th22;

      end;

      hence thesis by A0, A2, Th11, th22;

    end;

    theorem :: MATRIX11:24

    

     Th24: for p2, q2, pq2 st pq2 = (p2 * q2) holds ( sgn (pq2,K)) = (( sgn (p2,K)) * ( sgn (q2,K)))

    proof

      set n2 = (n + 2);

      let p,q,pq be Element of ( Permutations n2) such that

       A1: pq = (p * q);

      consider P2 be FinSequence of ( Group_of_Perm n2) such that

       A2: q = ( Product P2) and

       A3: for i st i in ( dom P2) holds ex trans be Element of ( Permutations n2) st (P2 . i) = trans & trans is being_transposition by Th21;

      consider P1 be FinSequence of ( Group_of_Perm n2) such that

       A4: p = ( Product P1) and

       A5: for i st i in ( dom P1) holds ex trans be Element of ( Permutations n2) st (P1 . i) = trans & trans is being_transposition by Th21;

      set PP = (P2 ^ P1);

      

       A6: for i st i in ( dom PP) holds ex trans be Element of ( Permutations n2) st (PP . i) = trans & trans is being_transposition

      proof

        let i such that

         A7: i in ( dom PP);

        now

          per cases by A7, FINSEQ_1: 25;

            suppose

             A8: i in ( dom P2);

            then (P2 . i) = (PP . i) by FINSEQ_1:def 7;

            hence thesis by A3, A8;

          end;

            suppose ex k be Nat st k in ( dom P1) & i = (( len P2) + k);

            then

            consider k be Nat such that

             A9: k in ( dom P1) and

             A10: i = (( len P2) + k);

            (P1 . k) = (PP . i) by A9, A10, FINSEQ_1:def 7;

            hence thesis by A5, A9;

          end;

        end;

        hence thesis;

      end;

      

       A11: ( Product PP) = (( Product P2) * ( Product P1)) by GROUP_4: 5

      .= pq by A1, A4, A2, MATRIX_1:def 13;

      now

        per cases by NAT_D: 12;

          suppose

           A12: (( len P1) mod 2) = 0 & (( len P2) mod 2) = 0 ;

          (( len PP) mod 2) = ((( len P2) + ( len P1)) mod 2) by FINSEQ_1: 22

          .= ((( 0 + ( len P1)) + 0 ) mod 2) by A12, NAT_D: 22

          .= 0 by A12;

          then

           A13: ( sgn (pq,K)) = ( 1_ K) by A11, A6, Th15;

          

           A14: ( sgn (q,K)) = ( 1_ K) by A2, A3, A12, Th15;

          ( sgn (p,K)) = ( 1_ K) by A4, A5, A12, Th15;

          hence thesis by A13, A14;

        end;

          suppose

           A15: (( len P1) mod 2) = 1 & (( len P2) mod 2) = 0 ;

          (( len PP) mod 2) = ((( len P2) + ( len P1)) mod 2) by FINSEQ_1: 22

          .= ((( 0 + ( len P1)) + 0 ) mod 2) by A15, NAT_D: 22

          .= 1 by A15;

          then

           A16: ( sgn (pq,K)) = ( - ( 1_ K)) by A11, A6, Th15;

          

           A17: ( sgn (q,K)) = ( 1_ K) by A2, A3, A15, Th15;

          ( sgn (p,K)) = ( - ( 1_ K)) by A4, A5, A15, Th15;

          hence thesis by A16, A17;

        end;

          suppose

           A18: (( len P1) mod 2) = 0 & (( len P2) mod 2) = 1;

          (( len PP) mod 2) = ((( len P2) + ( len P1)) mod 2) by FINSEQ_1: 22

          .= ((1 + ( len P1)) mod 2) by A18, NAT_D: 22

          .= ((1 + 0 ) mod 2) by A18, NAT_D: 22

          .= 1 by NAT_D: 14;

          then

           A19: ( sgn (pq,K)) = ( - ( 1_ K)) by A11, A6, Th15;

          

           A20: ( sgn (q,K)) = ( - ( 1_ K)) by A2, A3, A18, Th15;

          ( sgn (p,K)) = ( 1_ K) by A4, A5, A18, Th15;

          hence thesis by A19, A20;

        end;

          suppose

           A21: (( len P1) mod 2) = 1 & (( len P2) mod 2) = 1;

          (( len PP) mod 2) = ((( len P2) + ( len P1)) mod 2) by FINSEQ_1: 22

          .= ((1 + ( len P1)) mod 2) by A21, NAT_D: 22

          .= ((1 + 1) mod 2) by A21, NAT_D: 22

          .= 0 by NAT_D: 25;

          then

           A22: ( sgn (pq,K)) = ( 1_ K) by A11, A6, Th15;

          

           A23: (( 1_ K) * ( 1_ K)) = ( 1_ K);

          

           A24: ( sgn (q,K)) = ( - ( 1_ K)) by A2, A3, A21, Th15;

          ( sgn (p,K)) = ( - ( 1_ K)) by A4, A5, A21, Th15;

          hence thesis by A22, A24, A23, VECTSP_1: 10;

        end;

      end;

      hence thesis;

    end;

    

     Lm3: n < 2 implies p is even & p = ( idseq n)

    proof

      reconsider P = p as Permutation of ( Seg n) by MATRIX_1:def 12;

      assume

       A1: n < 2;

      now

        per cases by A1, NAT_1: 23;

          suppose

           A2: n = 0 ;

          then

           A3: ( Seg n) = {} ;

          

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

          P = {} by A2;

          hence thesis by A4, A3, MATRIX_1: 16, RELAT_1: 55;

        end;

          suppose

           A5: n = 1;

          

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

          P = ( id ( Seg n)) by A5, MATRIX_1: 10, TARSKI:def 1;

          hence thesis by A6, MATRIX_1: 16;

        end;

      end;

      hence thesis;

    end;

    registration

      cluster Fanoian non degenerated well-unital domRing-like commutative for Ring;

      existence

      proof

        set K = INT.Ring ;

        take K;

        K is Fanoian

        proof

          let a be Element of K;

          assume

           A1: (a + a) = ( 0. K);

          reconsider aa = a as Element of INT ;

          (aa + aa) = ( 0. K) by BINOP_2:def 20, A1;

          then (2 * aa) = 0 ;

          then aa = 0 ;

          then a = ( 0. K);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: MATRIX11:25

    

     Th25: (p is even & q is even or p is odd & q is odd iff (p * q) is even)

    proof

      reconsider pq = (p * q) as Element of ( Permutations n) by MATRIX_9: 39;

      now

        per cases ;

          suppose

           A1: n < 2;

          then pq is even by Lm3;

          hence thesis by A1, Lm3;

        end;

          suppose n >= 2;

          then

          reconsider n2 = (n - 2) as Nat by NAT_1: 21;

          set K = the Fanoian non degenerated well-unital domRing-like commutative Ring;

          reconsider p9 = p, q9 = q, pq as Element of ( Permutations (n2 + 2));

          thus p is even & q is even or p is odd & q is odd implies (p * q) is even

          proof

            assume p is even & q is even or p is odd & q is odd;

            then ( sgn (p9,K)) = ( 1_ K) & ( sgn (q9,K)) = ( 1_ K) or ( sgn (p9,K)) = ( - ( 1_ K)) & ( sgn (q9,K)) = ( - ( 1_ K)) by Th23;

            then

             A2: (( sgn (p9,K)) * ( sgn (q9,K))) = (( 1_ K) * ( 1_ K)) by VECTSP_1: 10;

            ( sgn (pq,K)) = ( 1_ K) by A2, Th24;

            hence thesis by Th23;

          end;

          thus (p * q) is even implies (p is even & q is even or p is odd & q is odd)

          proof

            assume (p * q) is even;

            then ( sgn (pq,K)) = ( 1_ K) by Th23;

            then

             A3: (( sgn (p9,K)) * ( sgn (q9,K))) = ( 1_ K) by Th24;

            assume

             A4: not (p is even & q is even or p is odd & q is odd);

            now

              per cases by A4;

                suppose

                 A5: p is even & q is odd;

                then

                 A6: ( sgn (q9,K)) = ( - ( 1_ K)) by Th23;

                ( sgn (p9,K)) = ( 1_ K) by A5, Th23;

                then (( sgn (p9,K)) * ( sgn (q9,K))) = ( - ( 1_ K)) by A6;

                hence thesis by A3, Th22;

              end;

                suppose

                 A7: p is odd & q is even;

                then

                 A8: ( sgn (q9,K)) = ( 1_ K) by Th23;

                ( sgn (p9,K)) = ( - ( 1_ K)) by A7, Th23;

                then (( sgn (p9,K)) * ( sgn (q9,K))) = ( - ( 1_ K)) by A8;

                hence thesis by A3, Th22;

              end;

            end;

            hence thesis;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: MATRIX11:26

    

     Th26: K is non degenerated well-unital domRing-like implies ( - (a,perm2)) = (( sgn (perm2,K)) * a)

    proof

      assume

       A0: K is non degenerated well-unital domRing-like;

      per cases ;

        suppose

         A1: perm2 is even & K is Fanoian;

        then

         A2: ( - (a,perm2)) = a by MATRIX_1:def 16;

        ( sgn (perm2,K)) = ( 1_ K) by A1, A0, Th23;

        hence thesis by A2;

      end;

        suppose

         A3: perm2 is odd & K is Fanoian;

        then

         A4: ( - (a,perm2)) = ( - a) by MATRIX_1:def 16;

        

         A5: (( - ( 1_ K)) * a) = ( - (( 1_ K) * a)) by VECTSP_1: 8;

        ( sgn (perm2,K)) = ( - ( 1_ K)) by A0, A3, Th23;

        hence thesis by A4, A5;

      end;

        suppose

         A6: perm2 is even & not K is Fanoian;

        then

         A7: ( - (a,perm2)) = a by MATRIX_1:def 16;

        

         A8: ( sgn (perm2,K)) = ( 1_ K) or ( sgn (perm2,K)) = ( - ( 1_ K)) by Th11;

        ( 1_ K) = ( - ( 1_ K)) by A0, A6, Th22;

        hence thesis by A7, A8;

      end;

        suppose

         A9: perm2 is odd & not K is Fanoian;

        then

         A10: ( - (a,perm2)) = ( - a) by MATRIX_1:def 16;

        

         A11: (( - ( 1_ K)) * a) = ( - (( 1_ K) * a)) by VECTSP_1: 8;

        

         A12: ( sgn (perm2,K)) = ( 1_ K) or ( sgn (perm2,K)) = ( - ( 1_ K)) by Th11;

        ( 1_ K) = ( - ( 1_ K)) by A0, A9, Th22;

        hence thesis by A10, A11, A12;

      end;

    end;

    theorem :: MATRIX11:27

    

     Th27: for tr be Element of ( Permutations (n + 2)) st tr is being_transposition holds tr is odd

    proof

      set K = the Fanoian Field;

      let tr be Element of ( Permutations (n + 2));

      assume tr is being_transposition;

      then ( sgn (tr,K)) = ( - ( 1_ K)) by Th14;

      hence thesis by Th23;

    end;

    registration

      let n;

      cluster odd for Permutation of ( Seg (n + 2));

      existence

      proof

        set n2 = (n + 2);

        

         A1: ( len ( Permutations n2)) = n2 by MATRIX_1: 9;

        n2 >= (2 + 0 ) by XREAL_1: 6;

        then {1, 2} in ( 2Set ( Seg n2)) by Th3;

        then

        consider i, j such that

         A2: i in ( Seg n2) and

         A3: j in ( Seg n2) and

         A4: i < j and {1, 2} = {i, j} by Th1;

        consider tr be Element of ( Permutations n2) such that

         A5: tr is being_transposition and (tr . i) = j by A2, A3, A4, Th16;

        tr is odd by A5, Th27;

        hence thesis by A1;

      end;

    end

    begin

    reserve pD for FinSequence of D,

M for Matrix of n, m, D,

pK,qK for FinSequence of K,

A for Matrix of n, K;

    definition

      let l, n, m, D;

      let M be Matrix of n, m, D;

      let pD be FinSequence of D;

      :: MATRIX11:def3

      func ReplaceLine (M,l,pD) -> Matrix of n, m, D means

      : Def3: ( len it ) = ( len M) & ( width it ) = ( width M) & for i, j st [i, j] in ( Indices M) holds (i <> l implies (it * (i,j)) = (M * (i,j))) & (i = l implies (it * (l,j)) = (pD . j)) if ( len pD) = ( width M)

      otherwise it = M;

      consistency ;

      existence

      proof

        thus ( len pD) = ( width M) implies ex M1 be Matrix of n, m, D st ( len M1) = ( len M) & ( width M1) = ( width M) & for i, j st [i, j] in ( Indices M) holds (i <> l implies (M1 * (i,j)) = (M * (i,j))) & (i = l implies (M1 * (l,j)) = (pD . j))

        proof

          reconsider M9 = M as Matrix of ( len M), ( width M), D by MATRIX_0: 51;

          reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;

          defpred P[ set, set, set] means for i, j st i = $1 & j = $2 holds (i <> l implies $3 = (M * (i,j))) & (i = l implies $3 = (pD . j));

          assume

           A1: ( len pD) = ( width M);

          

           A2: for i, j st [i, j] in [:( Seg n1), ( Seg m1):] holds ex x be Element of D st P[i, j, x]

          proof

            let i, j such that

             A3: [i, j] in [:( Seg n1), ( Seg m1):];

            now

              per cases ;

                case

                 A4: i = l;

                

                 A5: ( rng pD) c= D by FINSEQ_1:def 4;

                n1 <> 0 by A3, ZFMISC_1: 87;

                then ( len pD) = m by A1, MATRIX_0: 23;

                then j in ( Seg ( len pD)) by A3, ZFMISC_1: 87;

                then j in ( dom pD) by FINSEQ_1:def 3;

                then

                 A6: (pD . j) in ( rng pD) by FUNCT_1:def 3;

                 P[i, j, (pD . j)] by A4;

                hence thesis by A6, A5;

              end;

                case i <> l;

                then P[i, j, (M * (i,j))];

                hence thesis;

              end;

            end;

            hence thesis;

          end;

          consider M1 be Matrix of n1, m1, D such that

           A7: for i, j st [i, j] in ( Indices M1) holds P[i, j, (M1 * (i,j))] from MATRIX_0:sch 2( A2);

          reconsider M1 as Matrix of n, m, D;

          take M1;

           A8:

          now

            per cases ;

              suppose

               A9: n = 0 ;

              then ( len M1) = 0 by MATRIX_0:def 2;

              then

               A10: ( width M1) = 0 by MATRIX_0:def 3;

              ( len M) = 0 by A9, MATRIX_0:def 2;

              hence ( len M) = ( len M1) & ( width M1) = ( width M) by A9, A10, MATRIX_0:def 2, MATRIX_0:def 3;

            end;

              suppose

               A11: n > 0 ;

              then

               A12: ( width M) = m by MATRIX_0: 23;

              ( len M) = n by A11, MATRIX_0: 23;

              hence ( len M) = ( len M1) & ( width M) = ( width M1) by A11, A12, MATRIX_0: 23;

            end;

          end;

          ( Indices M9) = ( Indices M1) by MATRIX_0: 26;

          hence thesis by A7, A8;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of n, m, D;

        thus ( len pD) = ( width M) & (( len M1) = ( len M) & ( width M1) = ( width M) & for i, j st [i, j] in ( Indices M) holds (i <> l implies (M1 * (i,j)) = (M * (i,j))) & (i = l implies (M1 * (l,j)) = (pD . j))) & (( len M2) = ( len M) & ( width M2) = ( width M) & for i, j st [i, j] in ( Indices M) holds (i <> l implies (M2 * (i,j)) = (M * (i,j))) & (i = l implies (M2 * (l,j)) = (pD . j))) implies M1 = M2

        proof

          assume ( len pD) = ( width M);

          assume that

           A13: ( len M1) = ( len M) and

           A14: ( width M1) = ( width M) and

           A15: for i, j st [i, j] in ( Indices M) holds (i <> l implies (M1 * (i,j)) = (M * (i,j))) & (i = l implies (M1 * (l,j)) = (pD . j));

          assume that ( len M2) = ( len M) and ( width M2) = ( width M) and

           A16: for i, j st [i, j] in ( Indices M) holds (i <> l implies (M2 * (i,j)) = (M * (i,j))) & (i = l implies (M2 * (l,j)) = (pD . j));

          for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (M2 * (i,j))

          proof

            let i, j;

            assume [i, j] in ( Indices M1);

            then

             A17: [i, j] in ( Indices M) by A13, A14, MATRIX_4: 55;

            then

             A18: i = l implies (M1 * (l,j)) = (pD . j) by A15;

            

             A19: i <> l implies (M2 * (i,j)) = (M * (i,j)) by A16, A17;

            i <> l implies (M1 * (i,j)) = (M * (i,j)) by A15, A17;

            hence thesis by A16, A17, A18, A19;

          end;

          hence thesis by MATRIX_0: 27;

        end;

        thus thesis;

      end;

    end

    notation

      let l, n, m, D;

      let M be Matrix of n, m, D;

      let pD be FinSequence of D;

      synonym RLine (M,l,pD) for ReplaceLine (M,l,pD);

    end

    

     Lm4: for l, M, pD holds ( Indices M) = ( Indices ( RLine (M,l,pD))) & ( len M) = ( len ( RLine (M,l,pD))) & ( width M) = ( width ( RLine (M,l,pD)))

    proof

      let l, M, pD;

      now

        per cases ;

          case

           A1: ( len pD) = ( width M);

          then

           A2: ( width M) = ( width ( RLine (M,l,pD))) by Def3;

          ( len M) = ( len ( ReplaceLine (M,l,pD))) by A1, Def3;

          hence thesis by A2, MATRIX_4: 55;

        end;

          case ( len pD) <> ( width M);

          hence thesis by Def3;

        end;

      end;

      hence thesis;

    end;

    theorem :: MATRIX11:28

    

     Th28: for l, M, pD, i st i in ( Seg n) holds (i = l & ( len pD) = ( width M) implies ( Line (( RLine (M,l,pD)),i)) = pD) & (i <> l implies ( Line (( RLine (M,l,pD)),i)) = ( Line (M,i)))

    proof

      let l, M, pD, i such that

       A1: i in ( Seg n);

      set R = ( RLine (M,l,pD));

      set LR = ( Line (R,i));

      thus i = l & ( len pD) = ( width M) implies LR = pD

      proof

        assume that

         A2: i = l and

         A3: ( len pD) = ( width M);

        

         A4: ( width R) = ( len pD) by A3, Def3;

         A5:

        now

          let j be Nat such that

           A6: 1 <= j and

           A7: j <= ( len pD);

          

           A8: j in ( Seg ( width R)) by A4, A6, A7;

          n = ( len R) by MATRIX_0:def 2;

          then i in ( dom R) by A1, FINSEQ_1:def 3;

          then

           A9: [i, j] in ( Indices R) by A8, ZFMISC_1: 87;

          

           A10: ( Indices R) = ( Indices M) by Lm4;

          (LR . j) = (R * (i,j)) by A8, MATRIX_0:def 7;

          hence (LR . j) = (pD . j) by A2, A3, A9, A10, Def3;

        end;

        ( len LR) = ( len pD) by A4, MATRIX_0:def 7;

        hence thesis by A5;

      end;

      set LM = ( Line (M,i));

      

       A11: ( width M) = ( len LM) by MATRIX_0:def 7;

      

       A12: ( width M) = ( width R) by Lm4;

      assume

       A13: i <> l;

       A14:

      now

        let j be Nat such that

         A15: 1 <= j and

         A16: j <= ( len LM);

        

         A17: j in ( Seg ( len LM)) by A15, A16;

        then

         A18: (LM . j) = (M * (i,j)) by A11, MATRIX_0:def 7;

        i in ( Seg ( len M)) by A1, MATRIX_0:def 2;

        then i in ( dom M) by FINSEQ_1:def 3;

        then

         A19: [i, j] in ( Indices M) by A11, A17, ZFMISC_1: 87;

        

         A20: (LR . j) = (R * (i,j)) by A12, A11, A17, MATRIX_0:def 7;

        now

          per cases ;

            case ( len pD) = ( width M);

            hence (LM . j) = (LR . j) by A13, A18, A20, A19, Def3;

          end;

            case ( len pD) <> ( width M);

            hence (LM . j) = (LR . j) by Def3;

          end;

        end;

        hence (LM . j) = (LR . j);

      end;

      ( len LR) = ( width R) by MATRIX_0:def 7;

      hence thesis by A12, A11, A14;

    end;

    theorem :: MATRIX11:29

    for M, pD st ( len pD) = ( width M) holds for p9 be Element of (D * ) st pD = p9 holds ( RLine (M,l,pD)) = ( Replace (M,l,p9))

    proof

      let M, pD such that

       A1: ( len pD) = ( width M);

      set RL = ( RLine (M,l,pD));

      let p9 be Element of (D * ) such that

       A2: pD = p9;

      set R = ( Replace (M,l,p9));

      

       A3: ( len R) = ( len M) by FINSEQ_7: 5;

       A4:

      now

        let i be Nat such that

         A5: 1 <= i and

         A6: i <= ( len R);

        

         A7: i in ( Seg ( len R)) by A5, A6;

        then

         A8: i in ( dom R) by FINSEQ_1:def 3;

        

         A9: i in ( Seg n) by A3, A7, MATRIX_0:def 2;

        

         A10: i in ( dom M) by A3, A7, FINSEQ_1:def 3;

        now

          per cases ;

            case

             A11: i = l;

            then

             A12: ( Line (RL,i)) = pD by A1, A9, Th28;

            

             A13: (R /. i) = (R . i) by A8, PARTFUN1:def 6;

            (R /. i) = p9 by A3, A5, A6, A11, FINSEQ_7: 8;

            hence (R . i) = (RL . i) by A2, A9, A13, A12, MATRIX_0: 52;

          end;

            case

             A14: i <> l;

            then

             A15: ( Line (M,i)) = ( Line (RL,i)) by A9, Th28;

            

             A16: (R . i) = (R /. i) by A8, PARTFUN1:def 6;

            

             A17: (M . i) = ( Line (M,i)) by A9, MATRIX_0: 52;

            

             A18: (M /. i) = (M . i) by A10, PARTFUN1:def 6;

            (R /. i) = (M /. i) by A3, A5, A6, A14, FINSEQ_7: 10;

            hence (R . i) = (RL . i) by A9, A16, A18, A17, A15, MATRIX_0: 52;

          end;

        end;

        hence (R . i) = (RL . i);

      end;

      ( len M) = ( len RL) by Lm4;

      hence thesis by A4, FINSEQ_1: 14, FINSEQ_7: 5;

    end;

    theorem :: MATRIX11:30

    

     Th30: M = ( RLine (M,l,( Line (M,l))))

    proof

      set L = ( Line (M,l));

      set RL = ( RLine (M,l,L));

      

       A1: ( width M) = ( len L) by MATRIX_0:def 7;

       A2:

      now

        let i be Nat such that

         A3: 1 <= i and

         A4: i <= ( len M);

        

         A5: i in ( Seg ( len M)) by A3, A4;

        

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

        then

         A7: (RL . i) = ( Line (RL,i)) by A5, MATRIX_0: 52;

        

         A8: ( Line (M,i)) = (M . i) by A5, A6, MATRIX_0: 52;

        now

          per cases ;

            case i = l;

            hence (RL . i) = (M . i) by A1, A5, A6, A8, A7, Th28;

          end;

            case i <> l;

            hence (RL . i) = (M . i) by A5, A6, A8, A7, Th28;

          end;

        end;

        hence (RL . i) = (M . i);

      end;

      ( len M) = ( len RL) by Lm4;

      hence thesis by A2;

    end;

    

     Lm5: for K be Ring, pK be FinSequence of K holds for a be Element of K holds ( len pK) = ( len (a * pK))

    proof

      let K be Ring, pK be FinSequence of K;

      let a be Element of K;

      pK is Element of (( len pK) -tuples_on the carrier of K) by FINSEQ_2: 92;

      then (a * pK) is Element of (( len pK) -tuples_on the carrier of K) by FINSEQ_2: 113;

      hence thesis by CARD_1:def 7;

    end;

    

     Lm6: for pK, qK st ( len pK) = ( len qK) holds ( len pK) = ( len (pK + qK))

    proof

      let pK,qK be FinSequence of K;

      assume ( len pK) = ( len qK);

      then

       A1: qK is Element of (( len pK) -tuples_on the carrier of K) by FINSEQ_2: 92;

      pK is Element of (( len pK) -tuples_on the carrier of K) by FINSEQ_2: 92;

      then (pK + qK) is Element of (( len pK) -tuples_on the carrier of K) by A1, FINSEQ_2: 120;

      hence thesis by CARD_1:def 7;

    end;

    theorem :: MATRIX11:31

    

     Th31: for l, pK, qK, perm st l in ( Seg n) & ( len pK) = n & ( len qK) = n holds for M be Matrix of n, K holds (the multF of K $$ ( Path_matrix (perm,( RLine (M,l,((a * pK) + (b * qK))))))) = ((a * (the multF of K $$ ( Path_matrix (perm,( RLine (M,l,pK)))))) + (b * (the multF of K $$ ( Path_matrix (perm,( RLine (M,l,qK)))))))

    proof

      let l, pK, qK, perm such that

       A1: l in ( Seg n) and

       A2: ( len pK) = n and

       A3: ( len qK) = n;

      ( Seg n) <> {} by A1;

      then

       A4: n <> 0 ;

      reconsider L = l as Element of NAT by ORDINAL1:def 12;

      set mm = the multF of K;

      let M be Matrix of n, K;

      set Rpq = ( RLine (M,l,((a * pK) + (b * qK))));

      set Ppq = ( Path_matrix (perm,Rpq));

      

       A5: ( len Ppq) = n by MATRIX_3:def 7;

      then

      consider fpq be sequence of the carrier of K such that

       A6: (fpq . 1) = (Ppq . 1) and

       A7: for k be Nat st 0 <> k & k < ( len Ppq) holds (fpq . (k + 1)) = (mm . ((fpq . k),(Ppq . (k + 1)))) and

       A8: (mm $$ Ppq) = (fpq . ( len Ppq)) by A4, FINSOP_1:def 1;

      set Rq = ( RLine (M,l,qK));

      set Pq = ( Path_matrix (perm,Rq));

      

       A9: ( len Pq) = n by MATRIX_3:def 7;

      then

      consider fq be sequence of the carrier of K such that

       A10: (fq . 1) = (Pq . 1) and

       A11: for k be Nat st 0 <> k & k < ( len Pq) holds (fq . (k + 1)) = (mm . ((fq . k),(Pq . (k + 1)))) and

       A12: (mm $$ Pq) = (fq . ( len Pq)) by A4, FINSOP_1:def 1;

      set Rp = ( RLine (M,l,pK));

      set Pp = ( Path_matrix (perm,Rp));

      

       A13: ( len Pp) = n by MATRIX_3:def 7;

      then

      consider fp be sequence of the carrier of K such that

       A14: (fp . 1) = (Pp . 1) and

       A15: for k be Nat st 0 <> k & k < ( len Pp) holds (fp . (k + 1)) = (mm . ((fp . k),(Pp . (k + 1)))) and

       A16: (mm $$ Pp) = (fp . ( len Pp)) by A4, FINSOP_1:def 1;

      

       A17: n >= 1 by A4, NAT_1: 14;

      defpred P[ Nat] means (1 <= $1 & $1 < L) implies ((fp . $1) = (fq . $1) & (fpq . $1) = (fp . $1));

      

       A18: for k be Element of NAT st k in ( Seg n) holds (k <> L implies (Ppq . k) = (Pp . k) & (Pp . k) = (Pq . k)) & (k = L implies ex Ppk,Pqk be Element of K st Ppk = (Pp . k) & Pqk = (Pq . k) & (Ppq . k) = ((a * Ppk) + (b * Pqk)))

      proof

        let k be Element of NAT such that

         A19: k in ( Seg n);

        

         A20: (perm . k) in ( Seg n) by A19, MATRIX_7: 14;

        then

        reconsider pk = (perm . k) as Element of NAT ;

        

         A21: k in ( dom Pp) by A13, A19, FINSEQ_1:def 3;

        

         A22: k in ( dom Pq) by A9, A19, FINSEQ_1:def 3;

         [k, pk] in [:( Seg n), ( Seg n):] by A19, A20, ZFMISC_1: 87;

        then

         A23: [k, pk] in ( Indices M) by MATRIX_0: 24;

        ( dom qK) = ( Seg n) by A3, FINSEQ_1:def 3;

        then

         A24: (qK /. pk) = (qK . pk) by A19, MATRIX_7: 14, PARTFUN1:def 6;

        ( dom pK) = ( Seg n) by A2, FINSEQ_1:def 3;

        then (pK /. pk) = (pK . pk) by A19, MATRIX_7: 14, PARTFUN1:def 6;

        then

        reconsider ppk = (pK . pk), qpk = (qK . pk) as Element of K by A24;

        

         A25: ( len (b * qK)) = n by A3, Lm5;

        then ( dom (b * qK)) = ( Seg n) by FINSEQ_1:def 3;

        then

         A26: ((b * qK) . pk) = (b * qpk) by A19, FVSUM_1: 50, MATRIX_7: 14;

        

         A27: ( len (a * pK)) = n by A2, Lm5;

        then

         A28: ( len ((a * pK) + (b * qK))) = n by A25, Lm6;

        then

         A29: ( dom ((a * pK) + (b * qK))) = ( Seg n) by FINSEQ_1:def 3;

        ( dom (a * pK)) = ( Seg n) by A27, FINSEQ_1:def 3;

        then

         A30: ((a * pK) . pk) = (a * ppk) by A19, FVSUM_1: 50, MATRIX_7: 14;

        

         A31: ( width M) = n by MATRIX_0: 24;

        

         A32: k in ( dom Ppq) by A5, A19, FINSEQ_1:def 3;

        thus k <> L implies (Ppq . k) = (Pp . k) & (Pp . k) = (Pq . k)

        proof

          assume

           A33: k <> L;

          then

           A34: (Rq * (k,pk)) = (M * (k,pk)) by A3, A23, A31, Def3;

          (Rp * (k,pk)) = (M * (k,pk)) by A2, A23, A31, A33, Def3;

          then

           A35: (Pp . k) = (M * (k,pk)) by A21, MATRIX_3:def 7;

          (Rpq * (k,pk)) = (M * (k,pk)) by A28, A23, A31, A33, Def3;

          hence thesis by A32, A22, A34, A35, MATRIX_3:def 7;

        end;

        assume

         A36: k = L;

        then

         A37: (Rp * (k,pk)) = (pK . pk) by A2, A23, A31, Def3;

        

         A38: (Rq * (k,pk)) = (qK . pk) by A3, A23, A31, A36, Def3;

        take ppk, qpk;

        (Rpq * (k,pk)) = (((a * pK) + (b * qK)) . pk) by A28, A23, A31, A36, Def3;

        then (Rpq * (k,pk)) = ((a * ppk) + (b * qpk)) by A19, A29, A30, A26, FVSUM_1: 17, MATRIX_7: 14;

        hence thesis by A32, A21, A22, A37, A38, MATRIX_3:def 7;

      end;

      

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

      proof

        let k be Nat such that

         A40: P[k];

        set k1 = (k + 1);

        assume that

         A41: 1 <= k1 and

         A42: k1 < L;

        L <= n by A1, FINSEQ_1: 1;

        then

         A43: k1 <= n by A42, XXREAL_0: 2;

        then

         A44: k < n by NAT_1: 13;

        

         A45: k1 in ( Seg n) by A41, A43;

        now

          per cases ;

            case k = 0 ;

            hence thesis by A6, A14, A10, A18, A42, A45;

          end;

            case

             A46: k > 0 ;

            then

             A47: (fp . k1) = (mm . ((fp . k),(Pp . k1))) by A13, A15, A44;

            

             A48: 0 < (k + 0 ) by A46;

            

             A49: (fq . k1) = (mm . ((fq . k),(Pq . k1))) by A9, A11, A44, A46;

            (fpq . k1) = (mm . ((fpq . k),(Ppq . k1))) by A5, A7, A44, A46;

            hence thesis by A18, A40, A42, A45, A48, A47, A49, NAT_1: 13, NAT_1: 19;

          end;

        end;

        hence thesis;

      end;

      defpred Q[ Nat] means (1 <= $1 & L <= $1 & $1 <= n) implies for k be Nat st $1 = k holds (fpq . k) = ((a * (fp . k)) + (b * (fq . k)));

      

       A50: P[ 0 ];

      

       A51: (fpq . L) = ((a * (fp . L)) + (b * (fq . L)))

      proof

        consider PpL,PqL be Element of K such that

         A52: PpL = (Pp . L) and

         A53: PqL = (Pq . L) and

         A54: (Ppq . L) = ((a * PpL) + (b * PqL)) by A1, A18;

        

         A55: L >= 1 by A1, FINSEQ_1: 1;

        now

          per cases by A55, XXREAL_0: 1;

            case

             A56: L > 1;

            then

            reconsider L1 = (L - 1) as Element of NAT by NAT_1: 20;

            

             A57: (L1 + 1) > (1 + 0 ) by A56;

            

             A58: L1 < (L1 + 1) by NAT_1: 19;

            L <= n by A1, FINSEQ_1: 1;

            then

             A59: L1 < n by A58, XXREAL_0: 2;

            then (fp . L) = ((fp . L1) * PpL) by A13, A15, A52, A57;

            then

             A60: ((fp . L1) * (a * PpL)) = (a * (fp . L)) by GROUP_1:def 3;

            

             A61: for k be Nat holds P[k] from NAT_1:sch 2( A50, A39);

            

             A62: 1 <= L1 by A57, NAT_1: 19;

            then (fp . L1) = (fq . L1) by A61, A58;

            then (fq . L) = ((fp . L1) * PqL) by A9, A11, A53, A57, A59;

            then

             A63: ((fp . L1) * (b * PqL)) = (b * (fq . L)) by GROUP_1:def 3;

            (fpq . L1) = (fp . L1) by A61, A58, A62;

            then (fpq . L) = ((fp . L1) * ((a * PpL) + (b * PqL))) by A5, A7, A54, A57, A59;

            hence thesis by A60, A63, VECTSP_1:def 7;

          end;

            case L = 1;

            hence thesis by A6, A14, A10, A52, A53, A54;

          end;

        end;

        hence thesis;

      end;

      

       A64: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        let k be Nat such that

         A65: Q[k];

        set k1 = (k + 1);

        assume that

         A66: 1 <= k1 and

         A67: L <= k1 and

         A68: k1 <= n;

        let k9 be Nat such that

         A69: k9 = k1;

        now

          per cases by A67, XXREAL_0: 1;

            case k1 = L;

            hence thesis by A51, A69;

          end;

            case

             A70: k1 > L;

            

             A71: k1 in ( Seg n) by A66, A68;

            then

             A72: (Ppq . k1) = (Pp . k1) by A18, A70;

            k1 in ( dom Pp) by A13, A71, FINSEQ_1:def 3;

            then (Pp /. k1) = (Pp . k1) by PARTFUN1:def 6;

            then

            reconsider Ppk1 = (Pp . k1) as Element of K;

            

             A73: k < n by A68, NAT_1: 13;

            

             A74: ((b * (fq . k)) * Ppk1) = (b * ((fq . k) * Ppk1)) by GROUP_1:def 3;

            

             A75: ((a * (fp . k)) * Ppk1) = (a * ((fp . k) * Ppk1)) by GROUP_1:def 3;

            

             A76: 1 <= L by A1, FINSEQ_1: 1;

            

             A77: k >= L by A70, NAT_1: 13;

            then (fpq . k) = ((a * (fp . k)) + (b * (fq . k))) by A65, A68, A76, NAT_1: 13, XXREAL_0: 2;

            then

             A78: (fpq . k1) = (((a * (fp . k)) + (b * (fq . k))) * Ppk1) by A5, A7, A77, A73, A76, A72;

            (Pp . k1) = (Pq . k1) by A18, A70, A71;

            then

             A79: (fq . k1) = ((fq . k) * Ppk1) by A9, A11, A77, A73, A76;

            (fp . k1) = ((fp . k) * Ppk1) by A13, A15, A77, A73, A76;

            hence thesis by A69, A78, A79, A75, A74, VECTSP_1:def 7;

          end;

        end;

        hence thesis;

      end;

      

       A80: L <= n by A1, FINSEQ_1: 1;

      

       A81: Q[ 0 ];

      for k be Nat holds Q[k] from NAT_1:sch 2( A81, A64);

      hence thesis by A17, A5, A13, A9, A8, A16, A12, A80;

    end;

    theorem :: MATRIX11:32

    

     Th32: for l, pK, qK, perm st l in ( Seg n) & ( len pK) = n & ( len qK) = n holds for M be Matrix of n, K holds (( Path_product ( RLine (M,l,((a * pK) + (b * qK))))) . perm) = ((a * (( Path_product ( RLine (M,l,pK))) . perm)) + (b * (( Path_product ( RLine (M,l,qK))) . perm)))

    proof

      let l, pK, qK, perm such that

       A1: l in ( Seg n) and

       A2: ( len pK) = n and

       A3: ( len qK) = n;

      set mm = the multF of K;

      let M be Matrix of n, K;

      set Rpq = ( RLine (M,l,((a * pK) + (b * qK))));

      set Rp = ( RLine (M,l,pK));

      set Rq = ( RLine (M,l,qK));

      set Ppq = ( Path_matrix (perm,Rpq));

      set Pathpq = ( Path_product Rpq);

      set Pp = ( Path_matrix (perm,Rp));

      set Pathp = ( Path_product Rp);

      set Pq = ( Path_matrix (perm,Rq));

      set Pathq = ( Path_product Rq);

      now

        per cases ;

          case

           A4: perm is even;

          then (mm $$ Ppq) = ( - ((mm $$ Ppq),perm)) by MATRIX_1:def 16;

          then

           A5: (Pathpq . perm) = (mm $$ Ppq) by MATRIX_3:def 8;

          (mm $$ Pq) = ( - ((mm $$ Pq),perm)) by A4, MATRIX_1:def 16;

          then

           A6: (Pathq . perm) = (mm $$ Pq) by MATRIX_3:def 8;

          (mm $$ Pp) = ( - ((mm $$ Pp),perm)) by A4, MATRIX_1:def 16;

          then (Pathp . perm) = (mm $$ Pp) by MATRIX_3:def 8;

          hence thesis by A1, A2, A3, A6, A5, Th31;

        end;

          case

           A7: perm is odd;

          then ( - (mm $$ Ppq)) = ( - ((mm $$ Ppq),perm)) by MATRIX_1:def 16;

          then

           A8: (Pathpq . perm) = ( - (mm $$ Ppq)) by MATRIX_3:def 8;

          ( - (mm $$ Pp)) = ( - ((mm $$ Pp),perm)) by A7, MATRIX_1:def 16;

          then

           A9: (Pathp . perm) = ( - (mm $$ Pp)) by MATRIX_3:def 8;

          

           A10: ( - (a * (mm $$ Pp))) = (a * ( - (mm $$ Pp))) by VECTSP_1: 8;

          ( - (mm $$ Pq)) = ( - ((mm $$ Pq),perm)) by A7, MATRIX_1:def 16;

          then

           A11: (Pathq . perm) = ( - (mm $$ Pq)) by MATRIX_3:def 8;

          

           A12: ( - ((a * (mm $$ Pp)) + (b * (mm $$ Pq)))) = (( - (a * (mm $$ Pp))) - (b * (mm $$ Pq))) by VECTSP_1: 17;

          (mm $$ Ppq) = ((a * (mm $$ Pp)) + (b * (mm $$ Pq))) by A1, A2, A3, Th31;

          hence thesis by A9, A11, A8, A10, A12, VECTSP_1: 8;

        end;

      end;

      hence thesis;

    end;

    theorem :: MATRIX11:33

    

     Th33: for l, pK, qK st l in ( Seg n) & ( len pK) = n & ( len qK) = n holds for M be Matrix of n, K holds ( Det ( RLine (M,l,((a * pK) + (b * qK))))) = ((a * ( Det ( RLine (M,l,pK)))) + (b * ( Det ( RLine (M,l,qK)))))

    proof

      let l, pK, qK such that

       A1: l in ( Seg n) and

       A2: ( len pK) = n and

       A3: ( len qK) = n;

      set P = ( Permutations n);

      set KK = the carrier of K;

      set aa = the addF of K;

      let M be Matrix of n, K;

      set Rpq = ( RLine (M,l,((a * pK) + (b * qK))));

      set Rp = ( RLine (M,l,pK));

      set Rq = ( RLine (M,l,qK));

      set Pathpq = ( Path_product Rpq);

      set Pathp = ( Path_product Rp);

      set Pathq = ( Path_product Rq);

      set F = ( In (P,( Fin P)));

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

      then

       A4: F = P by SUBSET_1:def 8;

      then

      consider Gpq be Function of ( Fin P), KK such that

       A5: ( Det Rpq) = (Gpq . F) and

       A6: for e be Element of KK st e is_a_unity_wrt aa holds (Gpq . {} ) = e and

       A7: for x be Element of P holds (Gpq . {x}) = (Pathpq . x) and

       A8: for B9 be Element of ( Fin P) st B9 c= F & B9 <> {} holds for x be Element of P st x in (F \ B9) holds (Gpq . (B9 \/ {x})) = (aa . ((Gpq . B9),(Pathpq . x))) by SETWISEO:def 3;

      consider Gq be Function of ( Fin P), KK such that

       A9: ( Det Rq) = (Gq . F) and

       A10: for e be Element of KK st e is_a_unity_wrt aa holds (Gq . {} ) = e and

       A11: for x be Element of P holds (Gq . {x}) = (Pathq . x) and

       A12: for B9 be Element of ( Fin P) st B9 c= F & B9 <> {} holds for x be Element of P st x in (F \ B9) holds (Gq . (B9 \/ {x})) = (aa . ((Gq . B9),(Pathq . x))) by A4, SETWISEO:def 3;

      consider Gp be Function of ( Fin P), KK such that

       A13: ( Det Rp) = (Gp . F) and

       A14: for e be Element of KK st e is_a_unity_wrt aa holds (Gp . {} ) = e and

       A15: for x be Element of P holds (Gp . {x}) = (Pathp . x) and

       A16: for B9 be Element of ( Fin P) st B9 c= F & B9 <> {} holds for x be Element of P st x in (F \ B9) holds (Gp . (B9 \/ {x})) = (aa . ((Gp . B9),(Pathp . x))) by A4, SETWISEO:def 3;

      defpred P[ Nat] means for B be Element of ( Fin P) st ( card B) = $1 holds (Gpq . B) = ((a * (Gp . B)) + (b * (Gq . B)));

      

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

      proof

        let k be Nat such that

         A18: P[k];

        let B be Element of ( Fin P) such that

         A19: ( card B) = (k + 1);

        now

          per cases ;

            case k = 0 ;

            then

            consider x be object such that

             A20: B = {x} by A19, CARD_2: 42;

            

             A21: x in B by A20, TARSKI:def 1;

            B c= P by FINSUB_1:def 5;

            then

            reconsider x as Element of P by A21;

            

             A22: (Gp . B) = (Pathp . x) by A15, A20;

            

             A23: (Gq . B) = (Pathq . x) by A11, A20;

            (Gpq . B) = (Pathpq . x) by A7, A20;

            hence thesis by A1, A2, A3, A22, A23, Th32;

          end;

            case

             A24: k > 0 ;

            consider x be object such that

             A25: x in B by A19, CARD_1: 27, XBOOLE_0:def 1;

            B c= P by FINSUB_1:def 5;

            then

            reconsider x as Element of P by A25;

            B c= P by FINSUB_1:def 5;

            then (B \ {x}) c= P;

            then

            reconsider B9 = (B \ {x}) as Element of ( Fin P) by FINSUB_1:def 5;

            

             A26: not x in B9 by ZFMISC_1: 56;

            then

             A27: x in (F \ B9) by A4, XBOOLE_0:def 5;

            

             A28: ( {x} \/ B9) = B by A25, ZFMISC_1: 116;

            then

             A29: (k + 1) = (( card B9) + 1) by A19, A26, CARD_2: 41;

            then

             A30: (Gpq . B9) = ((a * (Gp . B9)) + (b * (Gq . B9))) by A18;

            

             A31: B9 c= F by A4, FINSUB_1:def 5;

            then (Gpq . B) = (aa . ((Gpq . B9),(Pathpq . x))) by A8, A24, A28, A29, A27, CARD_1: 27;

            

            then

             A32: (Gpq . B) = (((a * (Gp . B9)) + (b * (Gq . B9))) + ((a * (Pathp . x)) + (b * (Pathq . x)))) by A1, A2, A3, A30, Th32

            .= ((a * (Gp . B9)) + ((b * (Gq . B9)) + ((a * (Pathp . x)) + (b * (Pathq . x))))) by RLVECT_1:def 3

            .= ((a * (Gp . B9)) + ((a * (Pathp . x)) + ((b * (Gq . B9)) + (b * (Pathq . x))))) by RLVECT_1:def 3

            .= (((a * (Gp . B9)) + (a * (Pathp . x))) + ((b * (Gq . B9)) + (b * (Pathq . x)))) by RLVECT_1:def 3

            .= ((a * ((Gp . B9) + (Pathp . x))) + ((b * (Gq . B9)) + (b * (Pathq . x)))) by VECTSP_1:def 7

            .= ((a * (aa . ((Gp . B9),(Pathp . x)))) + (b * ((Gq . B9) + (Pathq . x)))) by VECTSP_1:def 7

            .= ((a * (aa . ((Gp . B9),(Pathp . x)))) + (b * (aa . ((Gq . B9),(Pathq . x)))));

            (Gp . B) = (aa . ((Gp . B9),(Pathp . x))) by A16, A24, A28, A29, A27, A31, CARD_1: 27;

            hence thesis by A12, A24, A28, A29, A27, A31, A32, CARD_1: 27;

          end;

        end;

        hence thesis;

      end;

      

       A33: P[ 0 ]

      proof

        let B be Element of ( Fin P);

        assume ( card B) = 0 ;

        then

         A34: B = {} ;

        then

         A35: (Gp . B) = ( 0. K) by A14, FVSUM_1: 6;

        

         A36: (Gq . B) = ( 0. K) by A10, A34, FVSUM_1: 6;

        (Gpq . B) = ( 0. K) by A6, A34, FVSUM_1: 6;

        hence thesis by A35, A36, RLVECT_1: 4;

      end;

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

      then P[( card F)];

      hence thesis by A5, A13, A9;

    end;

    theorem :: MATRIX11:34

    

     Th34: for K be commutative Ring, pK be FinSequence of K, a be Element of K, A be Matrix of n, K holds l in ( Seg n) & ( len pK) = n implies ( Det ( RLine (A,l,(a * pK)))) = (a * ( Det ( RLine (A,l,pK))))

    proof

      let K be commutative Ring, pK be FinSequence of K, a be Element of K, A be Matrix of n, K;

      assume that

       A1: l in ( Seg n) and

       A2: ( len pK) = n;

      pK is Element of (( len pK) -tuples_on the carrier of K) by FINSEQ_2: 92;

      then

       A3: ((a * pK) + (( 0. K) * pK)) = ((a + ( 0. K)) * pK) by FVSUM_1: 55;

      (a + ( 0. K)) = a by RLVECT_1: 4;

      

      hence ( Det ( RLine (A,l,(a * pK)))) = ((a * ( Det ( RLine (A,l,pK)))) + (( 0. K) * ( Det ( RLine (A,l,pK))))) by A1, A2, A3, Th33

      .= (a * ( Det ( RLine (A,l,pK)))) by RLVECT_1: 4;

    end;

    theorem :: MATRIX11:35

    l in ( Seg n) implies ( Det ( RLine (A,l,(a * ( Line (A,l)))))) = (a * ( Det A))

    proof

      

       A1: ( len ( Line (A,l))) = ( width A) by MATRIX_0:def 7;

      assume l in ( Seg n);

      then ( Det ( RLine (A,l,(a * ( Line (A,l)))))) = (a * ( Det ( RLine (A,l,( Line (A,l)))))) by A1, Th34, MATRIX_0: 24;

      hence thesis by Th30;

    end;

    theorem :: MATRIX11:36

    

     Th36: l in ( Seg n) & ( len pK) = n & ( len qK) = n implies ( Det ( RLine (A,l,(pK + qK)))) = (( Det ( RLine (A,l,pK))) + ( Det ( RLine (A,l,qK))))

    proof

      assume that

       A1: l in ( Seg n) and

       A2: ( len pK) = n and

       A3: ( len qK) = n;

      pK is Element of (( len pK) -tuples_on the carrier of K) by FINSEQ_2: 92;

      then

       A4: (( 1_ K) * pK) = pK by FVSUM_1: 57;

      qK is Element of (( len pK) -tuples_on the carrier of K) by A2, A3, FINSEQ_2: 92;

      then (( 1_ K) * qK) = qK by FVSUM_1: 57;

      

      hence ( Det ( RLine (A,l,(pK + qK)))) = ((( 1_ K) * ( Det ( RLine (A,l,pK)))) + (( 1_ K) * ( Det ( RLine (A,l,qK))))) by A1, A2, A3, A4, Th33

      .= (( Det ( RLine (A,l,pK))) + (( 1_ K) * ( Det ( RLine (A,l,qK)))))

      .= (( Det ( RLine (A,l,pK))) + ( Det ( RLine (A,l,qK))));

    end;

    

     Lm7: for F, M holds (M * F) is Matrix of n, m, D

    proof

      let F, M;

      

       A1: ( rng F) c= ( Seg n) by RELAT_1:def 19;

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

      then

       A2: ( dom M) = ( Seg n) by FINSEQ_1:def 3;

      ( dom F) = ( Seg n) by FUNCT_2: 52;

      then

       A3: ( dom (M * F)) = ( Seg n) by A1, A2, RELAT_1: 27;

      then

      reconsider Mp = (M * F) as FinSequence by FINSEQ_1:def 2;

      

       A4: for x st x in ( rng Mp) holds ex p be FinSequence of D st x = p & ( len p) = m

      proof

        

         A5: ( rng M) c= (D * ) by FINSEQ_1:def 4;

        let x such that

         A6: x in ( rng Mp);

        ( rng Mp) c= ( rng M) by RELAT_1: 26;

        then x in (D * ) by A6, A5;

        then

        reconsider p = x as FinSequence of D by FINSEQ_1:def 11;

        take p;

        p in ( rng M) by A6, FUNCT_1: 14;

        hence thesis by MATRIX_0:def 2;

      end;

      then

      reconsider Mp as Matrix of D by MATRIX_0: 9;

      

       A7: n is Element of NAT by ORDINAL1:def 12;

      ( len Mp) = n & for p be FinSequence of D st p in ( rng Mp) holds ( len p) = m

      proof

        thus ( len Mp) = n by A3, A7, FINSEQ_1:def 3;

        let p be FinSequence of D;

        assume p in ( rng Mp);

        then ex q be FinSequence of D st p = q & ( len q) = m by A4;

        hence thesis;

      end;

      hence thesis by MATRIX_0:def 2;

    end;

    begin

    definition

      let n, m, D;

      let F be Function of ( Seg n), ( Seg n);

      let M be Matrix of n, m, D;

      :: original: *

      redefine

      :: MATRIX11:def4

      func M * F -> Matrix of n, m, D means

      : Def4: ( len it ) = ( len M) & ( width it ) = ( width M) & for i, j, k st [i, j] in ( Indices M) & (F . i) = k holds (it * (i,j)) = (M * (k,j));

      compatibility

      proof

        reconsider Mf = (M * F) as Matrix of n, m, D by Lm7;

        let Mp be Matrix of n, m, D;

        thus Mp = (M * F) implies ( len Mp) = ( len M) & ( width Mp) = ( width M) & for i, j, k st [i, j] in ( Indices M) & (F . i) = k holds (Mp * (i,j)) = (M * (k,j))

        proof

          

           A1: ( rng F) c= ( Seg n) by RELAT_1:def 19;

          assume

           A2: Mp = (M * F);

          

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

          

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

           A5:

          now

            per cases ;

              case

               A6: n = 0 ;

              then ( width M) = 0 by A3, MATRIX_0:def 3;

              hence ( width M) = ( width Mp) by A4, A6, MATRIX_0:def 3;

            end;

              case

               A7: n > 0 ;

              then ( width M) = m by A3, MATRIX_0: 20;

              hence ( width M) = ( width Mp) by A4, A7, MATRIX_0: 20;

            end;

          end;

          hence ( len Mp) = ( len M) & ( width Mp) = ( width M) by A3, MATRIX_0:def 2;

          let i, j, k such that

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

           A9: (F . i) = k;

          ( Indices M) = [:( Seg n), ( Seg ( width M)):] by MATRIX_0: 25;

          then

           A10: i in ( Seg n) by A8, ZFMISC_1: 87;

          then

           A11: ( Line (Mp,i)) = (Mp . i) by MATRIX_0: 52;

          ( dom F) = ( Seg n) by FUNCT_2: 52;

          then

           A12: (F . i) in ( rng F) by A10, FUNCT_1:def 3;

          ( len Mp) = n by MATRIX_0: 25;

          then ( dom Mp) = ( Seg n) by FINSEQ_1:def 3;

          then (Mp . i) = (M . k) by A2, A9, A10, FUNCT_1: 12;

          then

           A13: ( Line (Mp,i)) = ( Line (M,k)) by A9, A12, A1, A11, MATRIX_0: 52;

          

           A14: j in ( Seg ( width M)) by A8, ZFMISC_1: 87;

          then (( Line (M,k)) . j) = (M * (k,j)) by MATRIX_0:def 7;

          hence thesis by A5, A14, A13, MATRIX_0:def 7;

        end;

        assume that

         A15: ( len Mp) = ( len M) and

         A16: ( width Mp) = ( width M);

        assume

         A17: for i, j, k st [i, j] in ( Indices M) & (F . i) = k holds (Mp * (i,j)) = (M * (k,j));

        for i, j st [i, j] in ( Indices Mp) holds (Mp * (i,j)) = (Mf * (i,j))

        proof

          

           A18: ( Indices Mp) = ( Indices M) by A15, A16, MATRIX_4: 55;

          let i, j such that

           A19: [i, j] in ( Indices Mp);

          ( Indices Mp) = [:( Seg n), ( Seg ( width M)):] by A16, MATRIX_0: 25;

          then

           A20: i in ( Seg n) by A19, ZFMISC_1: 87;

          then

           A21: ( Line (Mf,i)) = (Mf . i) by MATRIX_0: 52;

          

           A22: ( rng F) c= ( Seg n) by RELAT_1:def 19;

          ( dom F) = ( Seg n) by FUNCT_2: 52;

          then

           A23: (F . i) in ( rng F) by A20, FUNCT_1:def 3;

          then (F . i) in ( Seg n) by A22;

          then

          reconsider k = (F . i) as Element of NAT ;

          ( len Mf) = n by MATRIX_0: 25;

          then ( dom Mf) = ( Seg n) by FINSEQ_1:def 3;

          then (Mf . i) = (M . k) by A20, FUNCT_1: 12;

          then

           A24: ( Line (Mf,i)) = ( Line (M,k)) by A23, A22, A21, MATRIX_0: 52;

          

           A25: ( width M) = ( len ( Line (M,k))) by MATRIX_0:def 7;

          

           A26: ( width Mf) = ( len ( Line (Mf,i))) by MATRIX_0:def 7;

          

           A27: j in ( Seg ( width M)) by A16, A19, ZFMISC_1: 87;

          then (( Line (M,k)) . j) = (M * (k,j)) by MATRIX_0:def 7;

          then (Mf * (i,j)) = (M * (k,j)) by A27, A24, A25, A26, MATRIX_0:def 7;

          hence thesis by A17, A19, A18;

        end;

        hence thesis by MATRIX_0: 27;

      end;

      correctness by Lm7;

    end

    theorem :: MATRIX11:37

    

     Th37: ( Indices M) = ( Indices (M * F)) & for i, j st [i, j] in ( Indices M) holds ex k st (F . i) = k & [k, j] in ( Indices M) & ((M * F) * (i,j)) = (M * (k,j))

    proof

      set Mp = (M * F);

      

       A1: ( dom F) = ( Seg n) by FUNCT_2: 52;

      

       A2: ( width M) = ( width Mp) by Def4;

      ( len M) = ( len Mp) by Def4;

      hence ( Indices M) = ( Indices Mp) by A2, MATRIX_4: 55;

      let i, j such that

       A3: [i, j] in ( Indices M);

      ( Indices M) = [:( Seg n), ( Seg ( width M)):] by MATRIX_0: 25;

      then i in ( Seg n) by A3, ZFMISC_1: 87;

      then

       A4: (F . i) in ( rng F) by A1, FUNCT_1:def 3;

      

       A5: ( rng F) c= ( Seg n) by RELAT_1:def 19;

      then (F . i) in ( Seg n) by A4;

      then

      reconsider k = (F . i) as Element of NAT ;

      j in ( Seg ( width M)) by A3, ZFMISC_1: 87;

      then [k, j] in [:( Seg n), ( Seg ( width M)):] by A4, A5, ZFMISC_1: 87;

      then

       A6: [k, j] in ( Indices M) by MATRIX_0: 25;

      (Mp * (i,j)) = (M * (k,j)) by A3, Def4;

      hence thesis by A6;

    end;

    theorem :: MATRIX11:38

    

     Th38: for M be Matrix of n, m, D, F holds for k st k in ( Seg n) holds ( Line ((M * F),k)) = (M . (F . k))

    proof

      let M be Matrix of n, m, D, F;

      let k such that

       A1: k in ( Seg n);

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

      then k in ( dom (M * F)) by A1, FINSEQ_1:def 3;

      then ((M * F) . k) = (M . (F . k)) by FUNCT_1: 12;

      hence thesis by A1, MATRIX_0: 52;

    end;

    theorem :: MATRIX11:39

    

     Th39: (M * ( idseq n)) = M

    proof

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

      

       A1: ( width (M * I)) = ( width M) by Def4;

      

       A2: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = ((M * I) * (i,j))

      proof

        let i, j such that

         A3: [i, j] in ( Indices M);

         [i, j] in [:( Seg n), ( Seg ( width M)):] by A3, MATRIX_0: 25;

        then

         A4: i in ( Seg n) by ZFMISC_1: 87;

        ex k st (I . i) = k & [k, j] in ( Indices M) & ((M * I) * (i,j)) = (M * (k,j)) by A3, Th37;

        hence thesis by A4, FUNCT_1: 17;

      end;

      ( len (M * I)) = ( len M) by Def4;

      hence thesis by A1, A2, MATRIX_0: 21;

    end;

    theorem :: MATRIX11:40

    

     Th40: for p, Perm, q st q = (p * (Perm " )) holds ( Path_matrix (p,(A * Perm))) = (( Path_matrix (q,A)) * Perm)

    proof

      let p, Perm, q such that

       A1: q = (p * (Perm " ));

      reconsider perm = Perm as Element of ( Permutations n) by MATRIX_1:def 12;

      set Ap = (A * Perm);

      set P2 = ( Path_matrix (q,A));

      set P1 = ( Path_matrix (p,(A * Perm)));

      

       A2: ( dom perm) = ( Seg n) by FUNCT_2: 52;

      

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

      then

       A4: ( dom p) = ( Seg n) by FUNCT_2: 52;

      

       A5: ( rng p) = ( Seg n) by A3, FUNCT_2:def 3;

      

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

      then

       A7: ( dom q) = ( Seg n) by FUNCT_2: 52;

      ( len P2) = n by MATRIX_3:def 7;

      then

       A8: ( dom P2) = ( Seg n) by FINSEQ_1:def 3;

      

       A9: ( rng perm) = ( Seg n) by FUNCT_2:def 3;

      then

       A10: ( dom (P2 * perm)) = ( Seg n) by A2, A8, RELAT_1: 27;

      then

      reconsider P2p = (P2 * perm) as FinSequence by FINSEQ_1:def 2;

      

       A11: ( len P1) = n by MATRIX_3:def 7;

      

       A12: ( rng q) = ( Seg n) by A6, FUNCT_2:def 3;

       A13:

      now

        let k be Nat;

        assume that

         A14: 1 <= k and

         A15: k <= ( len P1);

        

         A16: k in ( Seg n) by A11, A14, A15;

        then

         A17: (p . k) in ( Seg n) by A4, A5, FUNCT_1: 3;

        then

        reconsider pk = (p . k) as Element of NAT ;

        

         A18: k = ((perm " ) . (perm . k)) by A2, A16, FUNCT_1: 34;

         [k, pk] in [:( Seg n), ( Seg n):] by A16, A17, ZFMISC_1: 87;

        then [k, pk] in ( Indices A) by MATRIX_0: 24;

        then

        consider permk be Nat such that

         A19: (perm . k) = permk and

         A20: [permk, pk] in ( Indices A) and

         A21: (Ap * (k,pk)) = (A * (permk,pk)) by Th37;

        ( dom P2p) = ( Seg n) by A2, A9, A8, RELAT_1: 27;

        then

         A22: (P2p . k) = (P2 . permk) by A16, A19, FUNCT_1: 12;

        ( Indices A) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        then

         A23: permk in ( Seg n) by A20, ZFMISC_1: 87;

        then (q . permk) in ( Seg n) by A7, A12, FUNCT_1: 3;

        then

        reconsider qpermk = (q . permk) as Element of NAT ;

        

         A24: (P2 . permk) = (A * (permk,qpermk)) by A8, A23, MATRIX_3:def 7;

        

         A25: ( dom P1) = ( Seg n) by A11, FINSEQ_1:def 3;

        (q . permk) = (p . ((perm " ) . (perm . k))) by A1, A7, A19, A23, FUNCT_1: 12;

        hence (P2p . k) = (P1 . k) by A16, A21, A24, A22, A18, A25, MATRIX_3:def 7;

      end;

      n is Element of NAT by ORDINAL1:def 12;

      then ( len P2p) = n by A10, FINSEQ_1:def 3;

      hence thesis by A11, A13, FINSEQ_1: 14;

    end;

    theorem :: MATRIX11:41

    

     Th41: for p, Perm, q st q = (p * (Perm " )) holds (the multF of K $$ ( Path_matrix (p,(A * Perm)))) = (the multF of K $$ ( Path_matrix (q,A)))

    proof

      let p, Perm, q such that

       A1: q = (p * (Perm " ));

      set mm = the multF of K;

      set P2 = ( Path_matrix (q,A));

      set P1 = ( Path_matrix (p,(A * Perm)));

      now

        per cases ;

          case

           A2: n = 0 ;

          then ( len P1) = 0 by MATRIX_3:def 7;

          then

           A3: (mm $$ P1) = ( the_unity_wrt mm) by FINSOP_1:def 1;

          ( len P2) = 0 by A2, MATRIX_3:def 7;

          hence thesis by A3, FINSOP_1:def 1;

        end;

          case (n + 0 ) > 0 ;

          then

           A4: n >= 1 by NAT_1: 19;

          

           A5: ( len P2) = n by MATRIX_3:def 7;

          

           A6: Perm is Element of ( Permutations n) by MATRIX_1:def 12;

          P1 = (P2 * Perm) by A1, Th40;

          hence thesis by A4, A5, A6, MATRIX_7: 33;

        end;

      end;

      hence thesis;

    end;

    theorem :: MATRIX11:42

    

     Th42: K is non degenerated domRing-like implies for p2, q2 st q2 = (p2 " ) holds ( sgn (p2,K)) = ( sgn (q2,K))

    proof

      assume

       A0: K is non degenerated domRing-like;

      

       A1: ((n + 1) + 1) >= ( 0 + 1) by XREAL_1: 6;

      let p2, q2;

      assume q2 = (p2 " );

      then

       A2: ( - (( 1_ K),p2)) = ( - (( 1_ K),q2)) by A1, MATRIX_7: 29;

      

       A3: ( - (( 1_ K),q2)) = (( sgn (q2,K)) * ( 1_ K)) by A0, Th26;

      ( - (( 1_ K),p2)) = (( sgn (p2,K)) * ( 1_ K)) by Th26, A0;

      then (( sgn (p2,K)) * ( 1_ K)) = ( sgn (q2,K)) by A2, A3, VECTSP_1:def 4;

      hence thesis;

    end;

    theorem :: MATRIX11:43

    

     Th43: K is non degenerated well-unital domRing-like implies for M be Matrix of (n + 2), K, perm2, Perm2 st perm2 = Perm2 holds for p2, q2 st q2 = (p2 * (Perm2 " )) holds (( Path_product M) . q2) = (( sgn (perm2,K)) * (( Path_product (M * Perm2)) . p2))

    proof

      assume

       A0: K is non degenerated well-unital domRing-like;

      let M be Matrix of (n + 2), K, perm2, Perm2 such that

       A1: perm2 = Perm2;

      set P = ( Permutations (n + 2));

      set mm = the multF of K;

      let p2, q2 such that

       A2: q2 = (p2 * (Perm2 " ));

      reconsider perm29 = (perm2 " ) as Element of P by MATRIX_7: 18;

      set PM = (mm $$ ( Path_matrix (q2,M)));

      set PMp = (mm $$ ( Path_matrix (p2,(M * Perm2))));

      ( sgn (q2,K)) = (( sgn (p2,K)) * ( sgn (perm29,K))) by A1, A2, Th24

      .= (( sgn (p2,K)) * ( sgn (perm2,K))) by A0, Th42;

      

      then ( - (PM,q2)) = ((( sgn (perm2,K)) * ( sgn (p2,K))) * PM) by A0, Th26

      .= (( sgn (perm2,K)) * (( sgn (p2,K)) * PM)) by GROUP_1:def 3

      .= (( sgn (perm2,K)) * (( sgn (p2,K)) * PMp)) by A2, Th41

      .= (( sgn (perm2,K)) * ( - (PMp,p2))) by Th26, A0

      .= (( sgn (perm2,K)) * (( Path_product (M * Perm2)) . p2)) by MATRIX_3:def 8;

      hence thesis by MATRIX_3:def 8;

    end;

    theorem :: MATRIX11:44

    

     Th44: for perm holds ex P be Permutation of ( Permutations n) st for p be Element of ( Permutations n) holds (P . p) = (p * perm)

    proof

      let perm;

      set P = ( Permutations n);

      defpred g[ object, object] means for p be Element of ( Permutations n) st $1 = p holds $2 = (p * perm);

      

       A1: ( card P) = ( card P);

      

       A2: for x be object st x in P holds ex y be object st y in P & g[x, y]

      proof

        let x be object;

        assume x in P;

        then

        reconsider p = x as Element of P;

        reconsider pp = (p * perm) as Element of P by MATRIX_9: 39;

        take pp;

        thus thesis;

      end;

      consider G be Function of P, P such that

       A3: for x be object st x in P holds g[x, (G . x)] from FUNCT_2:sch 1( A2);

      for x1,x2 be object st x1 in P & x2 in P & (G . x1) = (G . x2) holds x1 = x2

      proof

        let x1,x2 be object such that

         A4: x1 in P and

         A5: x2 in P and

         A6: (G . x1) = (G . x2);

        reconsider p1 = x1, p2 = x2 as Element of P by A4, A5;

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

        then

         A7: ( dom p2) = ( Seg n) by FUNCT_2: 52;

        

         A8: (G . p2) = (p2 * perm) by A3;

        

         A9: (G . p1) = (p1 * perm) by A3;

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

        then

         A10: ( rng perm) = ( Seg n) by FUNCT_2:def 3;

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

        then ( dom p1) = ( Seg n) by FUNCT_2: 52;

        

        then p1 = (p1 * ( id ( rng perm))) by A10, RELAT_1: 52

        .= (p1 * (perm * (perm " ))) by FUNCT_1: 39

        .= ((p2 * perm) * (perm " )) by A6, A9, A8, RELAT_1: 36

        .= (p2 * (perm * (perm " ))) by RELAT_1: 36

        .= (p2 * ( id ( rng perm))) by FUNCT_1: 39

        .= p2 by A10, A7, RELAT_1: 52;

        hence thesis;

      end;

      then

       A11: G is one-to-one by FUNCT_2: 19;

      G is onto by A11, A1, FINSEQ_4: 63;

      then

      reconsider G as Permutation of P by A11;

      take G;

      thus thesis by A3;

    end;

    theorem :: MATRIX11:45

    

     Th45: K is non degenerated domRing-like well-unital implies for M be Matrix of (n + 2), (n + 2), K, perm2, Perm2 st perm2 = Perm2 holds ( Det (M * Perm2)) = (( sgn (perm2,K)) * ( Det M))

    proof

      assume

       A0: K is non degenerated domRing-like well-unital;

      set n2 = (n + 2);

      let M be Matrix of n2, n2, K, perm2, Perm2 such that

       A1: perm2 = Perm2;

      set PathM = ( Path_product M);

      set Mperm = (M * Perm2);

      set P = ( Permutations n2);

      set KK = the carrier of K;

      set aa = the addF of K;

      set PathMp = ( Path_product Mperm);

      set F = ( In (P,( Fin P)));

      reconsider perm29 = (perm2 " ) as Element of P by MATRIX_7: 18;

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

      then

       A2: F = P by SUBSET_1:def 8;

      then

      consider GM be Function of ( Fin P), KK such that

       A3: ( Det M) = (GM . F) and for e be Element of KK st e is_a_unity_wrt aa holds (GM . {} ) = e and

       A4: for x be Element of P holds (GM . {x}) = (PathM . x) and

       A5: for B9 be Element of ( Fin P) st B9 c= F & B9 <> {} holds for x be Element of P st x in (F \ B9) holds (GM . (B9 \/ {x})) = (aa . ((GM . B9),(PathM . x))) by SETWISEO:def 3;

      consider PERM be Permutation of P such that

       A6: for p be Element of P holds (PERM . p) = (p * perm29) by Th44;

      consider GMp be Function of ( Fin P), KK such that

       A7: ( Det Mperm) = (GMp . F) and for e be Element of KK st e is_a_unity_wrt aa holds (GMp . {} ) = e and

       A8: for x be Element of P holds (GMp . {x}) = (PathMp . x) and

       A9: for B9 be Element of ( Fin P) st B9 c= F & B9 <> {} holds for x be Element of P st x in (F \ B9) holds (GMp . (B9 \/ {x})) = (aa . ((GMp . B9),(PathMp . x))) by A2, SETWISEO:def 3;

      defpred P[ Nat] means $1 <> 0 implies for B be Element of ( Fin P) st ( card B) = $1 holds (( sgn (perm2,K)) * (GMp . B)) = (GM . (PERM .: B));

      

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

      proof

        let k be Nat such that

         A11: P[k];

        set k1 = (k + 1);

        assume k1 <> 0 ;

        let B be Element of ( Fin P) such that

         A12: ( card B) = k1;

        per cases ;

          suppose k = 0 ;

          then

          consider x be object such that

           A13: B = {x} by A12, CARD_2: 42;

          

           A14: x in B by A13, TARSKI:def 1;

          B c= P by FINSUB_1:def 5;

          then

          reconsider x as Element of P by A14;

          

           A15: (GM . {(PERM . x)}) = (PathM . (PERM . x)) by A4;

          

           A16: (PERM . x) = (x * perm29) by A6;

          

           A17: P = ( dom PERM) by FUNCT_2: 52;

          (GMp . {x}) = (PathMp . x) by A8;

          then (( sgn (perm2,K)) * (GMp . B)) = (GM . {(PERM . x)}) by A0, A1, A13, A15, A16, Th43;

          then (( sgn (perm2,K)) * (GMp . B)) = (GM . ( Im (PERM,x))) by A17, FUNCT_1: 59;

          hence thesis by A13;

        end;

          suppose

           A18: k > 0 ;

          consider x be object such that

           A19: x in B by A12, CARD_1: 27, XBOOLE_0:def 1;

          B c= P by FINSUB_1:def 5;

          then

          reconsider x as Element of P by A19;

          (PERM .: (B \ {x})) c= ( rng PERM) by RELAT_1: 111;

          then

           A20: (PERM .: (B \ {x})) c= P by FUNCT_2:def 3;

          reconsider Px = (PERM . x) as Element of P;

          

           A21: Px in {Px} by TARSKI:def 1;

          ( dom PERM) = P by FUNCT_2: 52;

          then

           A22: ( Im (PERM,x)) = {Px} by FUNCT_1: 59;

          

           A23: B c= P by FINSUB_1:def 5;

          then (B \ {x}) c= P;

          then

          reconsider B9 = (B \ {x}), PeBx = (PERM .: (B \ {x})), PeB = (PERM .: B) as Element of ( Fin P) by A20, FINSUB_1:def 5;

          

           A24: ( {x} \/ B9) = B by A19, ZFMISC_1: 116;

          then

           A25: (PERM .: B) = (( Im (PERM,x)) \/ PeBx) by RELAT_1: 120;

          (PERM . x) = (x * perm29) by A6;

          then

           A26: (( sgn (perm2,K)) * (PathMp . x)) = (PathM . Px) by A1, Th43, A0;

          

           A27: ( dom PERM) = P by FUNCT_2: 52;

          B9 misses {x} by XBOOLE_1: 79;

          then (B9 /\ {x}) = {} ;

          then (PERM .: {} ) = ( {Px} /\ PeBx) by A22, FUNCT_1: 62;

          then not Px in PeBx by A21, XBOOLE_0:def 4;

          then

           A28: Px in (F \ PeBx) by A2, XBOOLE_0:def 5;

          

           A29: B9 c= P by FINSUB_1:def 5;

          

           A30: not x in B9 by ZFMISC_1: 56;

          then

           A31: x in (F \ B9) by A2, XBOOLE_0:def 5;

          

           A32: (k + 1) = (( card B9) + 1) by A12, A24, A30, CARD_2: 41;

          then ex y be object st y in B9 by A18, CARD_1: 27, XBOOLE_0:def 1;

          then (GM . PeB) = (aa . ((GM . PeBx),(PathM . Px))) by A2, A5, A20, A25, A22, A28, A29, A27;

          

          then (GM . PeB) = ((( sgn (perm2,K)) * (GMp . B9)) + (( sgn (perm2,K)) * (PathMp . x))) by A11, A18, A32, A26

          .= (( sgn (perm2,K)) * ((GMp . B9) + (PathMp . x))) by VECTSP_1:def 7

          .= (( sgn (perm2,K)) * (GMp . B)) by A2, A9, A18, A23, A24, A32, A31, CARD_1: 27, XBOOLE_1: 1;

          hence thesis;

        end;

      end;

      

       A33: P[ 0 ];

      

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

      

       A35: ( rng PERM) = P by FUNCT_2:def 3;

      

       A36: ( dom PERM) = P by FUNCT_2: 52;

      

       A37: (PERM .: ( dom PERM)) = ( rng PERM) by RELAT_1: 113;

      

       A38: (( 1_ K) * ( 1_ K)) = (( - ( 1_ K)) * ( - ( 1_ K))) by VECTSP_1: 10;

      

       A39: ( sgn (perm2,K)) = ( 1_ K) or ( sgn (perm2,K)) = ( - ( 1_ K)) by Th11;

      ( card F) <> 0 by A2;

      then (( sgn (perm2,K)) * ( Det Mperm)) = ( Det M) by A2, A3, A7, A34, A37, A36, A35;

      

      hence (( sgn (perm2,K)) * ( Det M)) = (( 1_ K) * ( Det Mperm)) by A39, A38, GROUP_1:def 3

      .= ( Det Mperm);

    end;

    theorem :: MATRIX11:46

    

     Th46: K is non degenerated well-unital domRing-like implies for M be Matrix of n, K, perm, Perm st perm = Perm holds ( Det (M * Perm)) = ( - (( Det M),perm))

    proof

      assume

       A0: K is non degenerated well-unital domRing-like;

      let M be Matrix of n, K, perm, Perm such that

       A1: Perm = perm;

      per cases ;

        suppose

         A2: n < 2;

        then perm = ( idseq n) by Lm3;

        then

         A3: (M * perm) = M by Th39;

        perm is even by A2, Lm3;

        hence thesis by A1, A3, MATRIX_1:def 16;

      end;

        suppose n >= 2;

        then

        reconsider n2 = (n - 2) as Nat by NAT_1: 21;

        reconsider M9 = M as Matrix of (n2 + 2), K;

        reconsider Perm2 = Perm as Permutation of ( Seg (n2 + 2));

        reconsider perm2 = perm as Element of ( Permutations (n2 + 2));

        ( Det (M9 * Perm2)) = (( sgn (perm2,K)) * ( Det M9)) by A0, A1, Th45;

        hence thesis by A0, Th26;

      end;

    end;

    theorem :: MATRIX11:47

    

     Th47: for PERM be Permutation of ( Permutations n), perm st perm is odd & for p holds (PERM . p) = (p * perm) holds (PERM .: { p : p is even }) = { q : q is odd }

    proof

      set P = ( Permutations n);

      let PERM be Permutation of P, perm such that

       A1: perm is odd and

       A2: for p holds (PERM . p) = (p * perm);

      set E = { p : p is even };

      set OD = { q : q is odd };

      for y be object holds y in OD iff ex x be object st x in ( dom PERM) & x in E & y = (PERM . x)

      proof

        let y be object;

        thus y in OD implies ex x be object st x in ( dom PERM) & x in E & y = (PERM . x)

        proof

          reconsider perm9 = (perm " ) as Element of P by MATRIX_7: 18;

          

           A3: ( dom PERM) = P by FUNCT_2: 52;

          n >= 2 by A1, Lm3;

          then

           A4: n >= 1 by XXREAL_0: 2;

          assume y in OD;

          then

          consider q such that

           A5: y = q and

           A6: q is odd;

          

           A7: (q * ( idseq n)) = q by MATRIX_1: 12;

          perm9 is odd by A1, A4, MATRIX_7: 28;

          then

           A8: (q * perm9) is even by A6, Th25;

          reconsider qp9 = (q * perm9) as Element of P by MATRIX_9: 39;

          take qp9;

          

           A9: (perm9 * perm) = ( idseq n) by MATRIX_1: 13;

          (PERM . qp9) = (qp9 * perm) by A2;

          hence thesis by A5, A3, A9, A7, A8, RELAT_1: 36;

        end;

        given x be object such that x in ( dom PERM) and

         A10: x in E and

         A11: y = (PERM . x);

        consider p such that

         A12: p = x and

         A13: p is even by A10;

        reconsider pp = (p * perm) as Element of P by MATRIX_9: 39;

        

         A14: (PERM . x) = (p * perm) by A2, A12;

        pp is odd by A1, A13, Th25;

        hence thesis by A11, A14;

      end;

      hence thesis by FUNCT_1:def 6;

    end;

    

     Lm8: for n, i, j st i in ( Seg n) & j in ( Seg n) & i < j holds ex ODD,EVEN be finite set st EVEN = { p : p is even } & ODD = { q : q is odd } & (EVEN /\ ODD) = {} & (EVEN \/ ODD) = ( Permutations n) & ex PERM be Function of EVEN, ODD, perm st perm is being_transposition & (perm . i) = j & ( dom PERM) = EVEN & PERM is bijective & for p st p in EVEN holds (PERM . p) = (p * perm)

    proof

      let n, i, j such that

       A1: i in ( Seg n) and

       A2: j in ( Seg n) and

       A3: i < j;

      set P = ( Permutations n);

      consider tr be Element of P such that

       A4: tr is being_transposition and

       A5: (tr . i) = j by A1, A2, A3, Th16;

       {i, j} in ( 2Set ( Seg n)) by A1, A2, A3, Th1;

      then

      reconsider n2 = (n - 2) as Nat by Th2, NAT_1: 21, NAT_1: 23;

      set ODD = { q : q is odd };

      set EVEN = { p : p is even };

      

       A6: EVEN c= P

      proof

        let x be object;

        assume x in EVEN;

        then ex p st p = x & p is even;

        hence thesis;

      end;

      

       A7: ODD c= P

      proof

        let x be object;

        assume x in ODD;

        then ex q st q = x & q is odd;

        hence thesis;

      end;

      then

      reconsider O = ODD, E = EVEN as finite set by A6;

      take O, E;

      thus E = { p : p is even } & O = { q : q is odd };

      thus (E /\ O) = {}

      proof

        assume (E /\ O) <> {} ;

        then

        consider x be object such that

         A8: x in (E /\ O) by XBOOLE_0:def 1;

        x in O by A8, XBOOLE_0:def 4;

        then

         A9: ex q st q = x & q is odd;

        x in E by A8, XBOOLE_0:def 4;

        then ex p st p = x & p is even;

        hence thesis by A9;

      end;

      thus (E \/ O) = P

      proof

        thus (E \/ O) c= P by A6, A7, XBOOLE_1: 8;

        let x be object;

        assume x in P;

        then

        reconsider p = x as Element of P;

        p is even or p is odd;

        then p in E or p in O;

        hence thesis by XBOOLE_0:def 3;

      end;

      consider PE be Permutation of P such that

       A10: for p holds (PE . p) = (p * tr) by Th44;

      set PERM = (PE | E);

      tr is Element of ( Permutations (n2 + 2));

      then (PE .: E) = O by A4, A10, Th27, Th47;

      then

       A11: ( rng PERM) = O by RELAT_1: 115;

      

       A12: ( dom PE) = P by FUNCT_2: 52;

      then

       A13: ( dom PERM) = E by A6, RELAT_1: 62;

      then

      reconsider PERM as Function of E, O by A11, FUNCT_2: 1;

      take PERM, tr;

      PERM is one-to-one onto by A11, FUNCT_1: 52, FUNCT_2:def 3;

      hence tr is being_transposition & (tr . i) = j & ( dom PERM) = E & PERM is bijective by A4, A5, A6, A12, RELAT_1: 62;

      let p;

      assume p in E;

      then (PERM . p) = (PE . p) by A13, FUNCT_1: 47;

      hence thesis by A10;

    end;

    theorem :: MATRIX11:48

    for n st n >= 2 holds ex ODD,EVEN be finite set st EVEN = { p : p is even } & ODD = { q : q is odd } & (EVEN /\ ODD) = {} & (EVEN \/ ODD) = ( Permutations n) & ( card EVEN) = ( card ODD)

    proof

      let n such that

       A1: n >= 2;

      1 <= n by A1, XXREAL_0: 2;

      then

       A2: 1 in ( Seg n);

      2 in ( Seg n) by A1;

      then

      consider O,E be finite set such that

       A3: E = { p : p is even } & O = { q : q is odd } and

       A4: (E /\ O) = {} & (E \/ O) = ( Permutations n) and

       A5: ex P be Function of E, O, perm st perm is being_transposition & (perm . 1) = 2 & ( dom P) = E & P is bijective & for p st p in E holds (P . p) = (p * perm) by A2, Lm8;

      consider P be Function of E, O, perm such that perm is being_transposition and (perm . 1) = 2 and

       A6: ( dom P) = E and

       A7: P is bijective and for p st p in E holds (P . p) = (p * perm) by A5;

      ( rng P) = O by A7, FUNCT_2:def 3;

      then (E,O) are_equipotent by A6, A7, WELLORD2:def 4;

      then ( card E) = ( card O) by CARD_1: 5;

      hence thesis by A3, A4;

    end;

    theorem :: MATRIX11:49

    

     Th49: K is non degenerated well-unital domRing-like implies for i, j st i in ( Seg n) & j in ( Seg n) & i < j holds for M be Matrix of n, K st ( Line (M,i)) = ( Line (M,j)) holds for p,q,tr be Element of ( Permutations n) st q = (p * tr) & tr is being_transposition & (tr . i) = j holds (( Path_product M) . q) = ( - (( Path_product M) . p))

    proof

      assume

       A0: K is non degenerated well-unital domRing-like;

      let i, j such that

       A1: i in ( Seg n) and

       A2: j in ( Seg n) and

       A3: i < j;

       {i, j} in ( 2Set ( Seg n)) by A1, A2, A3, Th1;

      then

      reconsider n2 = (n - 2) as Nat by Th2, NAT_1: 21, NAT_1: 23;

      let M be Matrix of n, K such that

       A4: ( Line (M,i)) = ( Line (M,j));

      reconsider M9 = M as Matrix of (n2 + 2), K;

      let p,q,tr be Element of ( Permutations n) such that

       A5: q = (p * tr) and

       A6: tr is being_transposition and

       A7: (tr . i) = j;

      reconsider TR = tr as Permutation of ( Seg (n2 + 2)) by MATRIX_1:def 12;

      set Mt = (M9 * TR);

      

       A8: for k be Nat st 1 <= k & k <= ( len M9) holds (M9 . k) = (Mt . k)

      proof

        let k be Nat such that

         A9: 1 <= k and

         A10: k <= ( len M9);

        

         A11: k in ( Seg ( len M9)) by A9, A10;

        

         A12: ( Line (M,j)) = (M . j) by A2, MATRIX_0: 52;

        

         A13: ( dom TR) = ( Seg n) by FUNCT_2: 52;

        

         A14: ( Line (M,i)) = (M . i) by A1, MATRIX_0: 52;

        

         A15: ( len M9) = n by MATRIX_0:def 2;

        then

         A16: ( Line (Mt,k)) = (M . (tr . k)) by A11, Th38;

        per cases ;

          suppose k = i;

          hence thesis by A1, A4, A7, A16, A14, A12, MATRIX_0: 52;

        end;

          suppose

           A17: k = j;

          then

           A18: (M . k) = (M . i) by A2, A4, A14, MATRIX_0: 52;

          ( Line (Mt,k)) = (M . i) by A3, A6, A7, A16, A17, Th8;

          hence thesis by A2, A17, A18, MATRIX_0: 52;

        end;

          suppose k <> i & k <> j;

          then ( Line (Mt,k)) = (M . k) by A3, A6, A7, A11, A15, A13, A16, Th8;

          hence thesis by A11, A15, MATRIX_0: 52;

        end;

      end;

      ( len Mt) = ( len M9) by Def4;

      then

       A19: Mt = M by A8;

      reconsider Tr = tr, p2 = p as Element of ( Permutations (n2 + 2));

      

       A20: ( sgn (Tr,K)) = ( - ( 1_ K)) by A6, Th14;

      tr = (tr " ) by A6, Th20;

      

      hence (( Path_product M) . q) = (( - ( 1_ K)) * (( Path_product M9) . p2)) by A0, A5, A19, A20, Th43

      .= ( - (( 1_ K) * (( Path_product M9) . p2))) by VECTSP_1: 9

      .= ( - (( Path_product M) . p));

    end;

    theorem :: MATRIX11:50

    

     Th50: K is non degenerated well-unital domRing-like implies for i, j st i in ( Seg n) & j in ( Seg n) & i < j holds for M be Matrix of n, K st ( Line (M,i)) = ( Line (M,j)) holds ( Det M) = ( 0. K)

    proof

      assume

       A0: K is non degenerated well-unital domRing-like;

      let i, j such that

       A1: i in ( Seg n) and

       A2: j in ( Seg n) and

       A3: i < j;

      set P = ( Permutations n);

      consider Q,E be finite set such that E = { p : p is even } & Q = { q : q is odd } and

       A4: (E /\ Q) = {} & (E \/ Q) = P and

       A5: ex P be Function of E, Q, tr be Element of ( Permutations n) st tr is being_transposition & (tr . i) = j & ( dom P) = E & P is bijective & for p st p in E holds (P . p) = (p * tr) by A1, A2, A3, Lm8;

      

       A6: E c= P by A4, XBOOLE_1: 7;

      set KK = the carrier of K;

      set aa = the addF of K;

      let M be Matrix of n, K such that

       A7: ( Line (M,i)) = ( Line (M,j));

      

       A8: Q c= P by A4, XBOOLE_1: 7;

      set PathM = ( Path_product M);

      consider PERM be Function of E, Q, tr be Element of ( Permutations n) such that

       A9: tr is being_transposition and

       A10: (tr . i) = j and

       A11: ( dom PERM) = E and

       A12: PERM is bijective and

       A13: for p st p in E holds (PERM . p) = (p * tr) by A5;

      reconsider E, Q as Element of ( Fin P) by A6, A8, FINSUB_1:def 5;

      aa is having_a_unity by FVSUM_1: 8;

      then

      consider GE be Function of ( Fin P), KK such that

       A14: (aa $$ (E,PathM)) = (GE . E) and

       A15: for e be Element of KK st e is_a_unity_wrt aa holds (GE . {} ) = e and

       A16: for x be Element of P holds (GE . {x}) = (PathM . x) and

       A17: for B9 be Element of ( Fin P) st B9 c= E & B9 <> {} holds for x be Element of P st x in (E \ B9) holds (GE . (B9 \/ {x})) = (aa . ((GE . B9),(PathM . x))) by SETWISEO:def 3;

      

       A18: E misses Q by A4;

      aa is having_a_unity by FVSUM_1: 8;

      then

      consider GQ be Function of ( Fin P), KK such that

       A19: (aa $$ (Q,PathM)) = (GQ . Q) and

       A20: for e be Element of KK st e is_a_unity_wrt aa holds (GQ . {} ) = e and

       A21: for x be Element of P holds (GQ . {x}) = (PathM . x) and

       A22: for B9 be Element of ( Fin P) st B9 c= Q & B9 <> {} holds for x be Element of P st x in (Q \ B9) holds (GQ . (B9 \/ {x})) = (aa . ((GQ . B9),(PathM . x))) by SETWISEO:def 3;

      defpred P[ Nat] means for B,PB be Element of ( Fin P) st ( card B) = $1 & B c= E & (PERM .: B) = PB holds ((GE . B) + (GQ . PB)) = ( 0. K);

      

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

      proof

        let k be Nat such that

         A24: P[k];

        let B,PB be Element of ( Fin P) such that

         A25: ( card B) = (k + 1) and

         A26: B c= E and

         A27: (PERM .: B) = PB;

        now

          per cases ;

            case k = 0 ;

            then

            consider x be object such that

             A28: B = {x} by A25, CARD_2: 42;

            

             A29: x in B by A28, TARSKI:def 1;

            B c= P by FINSUB_1:def 5;

            then

            reconsider x as Element of P by A29;

            (x * tr) is Element of P by MATRIX_9: 39;

            then

            reconsider Px = (PERM . x) as Element of P by A13, A26, A29;

            

             A30: ( Im (PERM,x)) = {Px} by A11, A26, A29, FUNCT_1: 59;

            

             A31: (GE . {x}) = (PathM . x) by A16;

            

             A32: (GQ . {(PERM . x)}) = (PathM . Px) by A21;

            Px = (x * tr) by A13, A26, A29;

            then ( - (GE . B)) = (GQ . PB) by A0, A1, A2, A3, A7, A9, A10, A27, A28, A31, A32, A30, Th49;

            hence thesis by RLVECT_1:def 10;

          end;

            case

             A33: k > 0 ;

            consider x be object such that

             A34: x in B by A25, CARD_1: 27, XBOOLE_0:def 1;

            B c= P by FINSUB_1:def 5;

            then

            reconsider x as Element of P by A34;

            (x * tr) is Element of P by MATRIX_9: 39;

            then

            reconsider Px = (PERM . x) as Element of P by A13, A26, A34;

            

             A35: ( Im (PERM,x)) = {Px} by A11, A26, A34, FUNCT_1: 59;

            Px = (x * tr) by A13, A26, A34;

            then

             A36: ( - (PathM . x)) = (PathM . Px) by A0, A1, A2, A3, A7, A9, A10, Th49;

            

             A37: Q c= P by FINSUB_1:def 5;

            B c= P by FINSUB_1:def 5;

            then

             A38: (B \ {x}) c= P;

            

             A39: ( rng PERM) = Q by A12, FUNCT_2:def 3;

            then

             A40: Px in Q by A11, A26, A34, FUNCT_1:def 3;

            (PERM .: (B \ {x})) c= ( rng PERM) by RELAT_1: 111;

            then (PERM .: (B \ {x})) c= P by A39, A37;

            then

            reconsider B9 = (B \ {x}), PeBx = (PERM .: (B \ {x})) as Element of ( Fin P) by A38, FINSUB_1:def 5;

            

             A41: Px in {Px} by TARSKI:def 1;

            

             A42: ( {x} \/ B9) = B by A34, ZFMISC_1: 116;

            then

             A43: (PERM .: B) = (( Im (PERM,x)) \/ PeBx) by RELAT_1: 120;

            B9 misses {x} by XBOOLE_1: 79;

            then (B9 /\ {x}) = {} ;

            then (PERM .: {} ) = ( {Px} /\ PeBx) by A12, A35, FUNCT_1: 62;

            then not Px in PeBx by A41, XBOOLE_0:def 4;

            then

             A44: Px in (Q \ PeBx) by A40, XBOOLE_0:def 5;

            

             A45: not x in B9 by ZFMISC_1: 56;

            then

             A46: x in (E \ B9) by A26, A34, XBOOLE_0:def 5;

            

             A47: (k + 1) = (( card B9) + 1) by A25, A42, A45, CARD_2: 41;

            then

            consider y be object such that

             A48: y in B9 by A33, CARD_1: 27, XBOOLE_0:def 1;

            (B \ {x}) c= E by A26;

            then (PERM . y) in PeBx by A11, A48, FUNCT_1:def 6;

            then (GQ . PB) = (aa . ((GQ . PeBx),(PathM . Px))) by A22, A27, A39, A43, A35, A44, RELAT_1: 111;

            

            hence ((GQ . PB) + (GE . B)) = (((GQ . PeBx) - (PathM . x)) + ((GE . B9) + (PathM . x))) by A17, A26, A33, A42, A47, A46, A36, CARD_1: 27, XBOOLE_1: 1

            .= ((GQ . PeBx) + (( - (PathM . x)) + ((GE . B9) + (PathM . x)))) by RLVECT_1:def 3

            .= ((GQ . PeBx) + ((GE . B9) + ((PathM . x) - (PathM . x)))) by RLVECT_1:def 3

            .= ((GQ . PeBx) + ((GE . B9) + ( 0. K))) by RLVECT_1:def 10

            .= (((GQ . PeBx) + (GE . B9)) + ( 0. K)) by RLVECT_1:def 3

            .= (( 0. K) + ( 0. K)) by A24, A26, A47, XBOOLE_1: 1

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

          end;

        end;

        hence thesis;

      end;

      set F = ( In (P,( Fin P)));

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

      then

       A49: P = F by SUBSET_1:def 8;

      ( rng PERM) = Q by A12, FUNCT_2:def 3;

      then

       A50: (PERM .: E) = Q by A11, RELAT_1: 113;

      

       A51: P[ 0 ]

      proof

        let B,PB be Element of ( Fin P) such that

         A52: ( card B) = 0 and B c= E and

         A53: (PERM .: B) = PB;

        

         A54: B = {} by A52;

        then

         A55: (GE . B) = ( 0. K) by A15, FVSUM_1: 6;

        (PERM .: {} ) = {} ;

        then (GQ . PB) = ( 0. K) by A20, A53, A54, FVSUM_1: 6;

        hence thesis by A55, RLVECT_1:def 4;

      end;

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

      then P[( card E)];

      then ((aa $$ (E,PathM)) + (aa $$ (Q,PathM))) = ( 0. K) by A14, A19, A50;

      hence thesis by A4, A18, A49, FVSUM_1: 8, SETWOP_2: 4;

    end;

    theorem :: MATRIX11:51

    

     Th51: K is non degenerated well-unital domRing-like implies for i, j st i in ( Seg n) & j in ( Seg n) & i <> j holds ( Det ( RLine (A,i,( Line (A,j))))) = ( 0. K)

    proof

      assume

       A0: K is non degenerated well-unital domRing-like;

      let i, j such that

       A1: i in ( Seg n) and

       A2: j in ( Seg n) and

       A3: i <> j;

      

       A4: i < j or j < i by A3, XXREAL_0: 1;

      ( len ( Line (A,j))) = ( width A) by MATRIX_0:def 7;

      then

       A5: ( Line (( RLine (A,i,( Line (A,j)))),i)) = ( Line (A,j)) by A1, Th28;

      ( Line (( RLine (A,i,( Line (A,j)))),j)) = ( Line (A,j)) by A2, A3, Th28;

      hence thesis by A1, A2, A5, A4, A0, Th50;

    end;

    theorem :: MATRIX11:52

    

     Th52: K is non degenerated well-unital domRing-like implies for i, j st i in ( Seg n) & j in ( Seg n) & i <> j holds ( Det ( RLine (A,i,(a * ( Line (A,j)))))) = ( 0. K)

    proof

      assume

       A0: K is non degenerated well-unital domRing-like;

      let i, j such that

       A1: i in ( Seg n) and

       A2: j in ( Seg n) and

       A3: i <> j;

      ( width A) = n by MATRIX_0: 24;

      then ( len ( Line (A,j))) = n by MATRIX_0:def 7;

      

      hence ( Det ( RLine (A,i,(a * ( Line (A,j)))))) = (a * ( Det ( RLine (A,i,( Line (A,j)))))) by A1, Th34

      .= (a * ( 0. K)) by A0, A1, A2, A3, Th51

      .= ( 0. K);

    end;

    theorem :: MATRIX11:53

    K is non degenerated well-unital domRing-like implies for i, j st i in ( Seg n) & j in ( Seg n) & i <> j holds ( Det A) = ( Det ( RLine (A,i,(( Line (A,i)) + (a * ( Line (A,j)))))))

    proof

      assume

       A0: K is non degenerated well-unital domRing-like;

      let i, j such that

       A1: i in ( Seg n) and

       A2: j in ( Seg n) and

       A3: i <> j;

      

       A4: ( width A) = n by MATRIX_0: 24;

      then

       A5: ( len ( Line (A,j))) = n by MATRIX_0:def 7;

      

       A6: ( len ( Line (A,j))) = ( len (a * ( Line (A,j)))) by Lm5;

      ( len ( Line (A,i))) = n by A4, MATRIX_0:def 7;

      

      hence ( Det ( RLine (A,i,(( Line (A,i)) + (a * ( Line (A,j))))))) = (( Det ( RLine (A,i,( Line (A,i))))) + ( Det ( RLine (A,i,(a * ( Line (A,j))))))) by A1, A5, A6, Th36

      .= (( Det A) + ( Det ( RLine (A,i,(a * ( Line (A,j))))))) by Th30

      .= (( Det A) + ( 0. K)) by A0, A1, A2, A3, Th52

      .= ( Det A) by RLVECT_1: 4;

    end;

    theorem :: MATRIX11:54

    

     Th54: K is non degenerated well-unital domRing-like & not F in ( Permutations n) implies ( Det (A * F)) = ( 0. K)

    proof

      assume

       A0: K is non degenerated well-unital domRing-like;

      assume not F in ( Permutations n);

      then

       A1: not F is onto or not F is one-to-one by MATRIX_1:def 12;

      ( card ( Seg n)) = ( card ( Seg n));

      then not F is one-to-one by A1, FINSEQ_4: 63;

      then

      consider x,y be object such that

       A2: x in ( dom F) and

       A3: y in ( dom F) and

       A4: (F . x) = (F . y) and

       A5: x <> y by FUNCT_1:def 4;

      

       A6: ( dom F) = ( Seg n) by FUNCT_2: 52;

      then

      reconsider x, y as Nat by A2, A3;

      ( Line ((A * F),x)) = (A . (F . x)) by A2, A6, Th38;

      then

       A7: ( Line ((A * F),x)) = ( Line ((A * F),y)) by A3, A4, A6, Th38;

      x > y or y > x by A5, XXREAL_0: 1;

      hence thesis by A2, A0, A3, A6, A7, Th50;

    end;

    begin

    definition

      let K be non empty addLoopStr;

      :: MATRIX11:def5

      func addFinS (K) -> BinOp of (the carrier of K * ) means

      : Def5: for p1,p2 be Element of (the carrier of K * ) holds (it . (p1,p2)) = (p1 + p2);

      existence

      proof

        set KK = the carrier of K;

        defpred ADD[ set, set, set] means for p1,p2 be Element of (KK * ) st $1 = p1 & $2 = p2 holds $3 = (p1 + p2);

        

         A1: for x be Element of (KK * ) holds for y be Element of (KK * ) holds ex z be Element of (KK * ) st ADD[x, y, z]

        proof

          let x be Element of (KK * );

          let y be Element of (KK * );

          reconsider p1 = x, p2 = y as FinSequence of KK;

          reconsider pp = (p1 + p2) as Element of (KK * ) by FINSEQ_1:def 11;

          take pp;

          thus thesis;

        end;

        consider A be Function of [:(KK * ), (KK * ):], (KK * ) such that

         A2: for x be Element of (KK * ) holds for y be Element of (KK * ) holds ADD[x, y, (A . (x,y))] from BINOP_1:sch 3( A1);

        take A;

        thus thesis by A2;

      end;

      uniqueness

      proof

        set KK = the carrier of K;

        let f1,f2 be Function of [:(KK * ), (KK * ):], (KK * ) such that

         A3: for p1,p2 be Element of (KK * ) holds (f1 . (p1,p2)) = (p1 + p2) and

         A4: for p1,p2 be Element of (KK * ) holds (f2 . (p1,p2)) = (p1 + p2);

        now

          let p1 be Element of (KK * );

          let p2 be Element of (KK * );

          (f1 . (p1,p2)) = (p1 + p2) by A3;

          hence (f1 . (p1,p2)) = (f2 . (p1,p2)) by A4;

        end;

        hence thesis;

      end;

    end

    

     Lm9: for K be non empty addLoopStr holds for p1,p2 be Element of (the carrier of K * ) holds ( dom (p1 + p2)) = (( dom p1) /\ ( dom p2))

    proof

      let K be non empty addLoopStr;

      let p1,p2 be Element of (the carrier of K * );

      

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

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

      then [:( rng p1), ( rng p2):] c= [:the carrier of K, the carrier of K:] by A1, ZFMISC_1: 96;

      then [:( rng p1), ( rng p2):] c= ( dom the addF of K) by FUNCT_2:def 1;

      hence thesis by FUNCOP_1: 69;

    end;

    registration

      let K be Abelian non empty addLoopStr;

      cluster ( addFinS K) -> commutative;

      coherence

      proof

        set KK = the carrier of K;

        let p1,p2 be Element of (KK * );

        

         A1: ( rng p2) c= KK by FINSEQ_1:def 4;

        

         A2: ( dom (p1 + p2)) = (( dom p1) /\ ( dom p2)) by Lm9;

        

         A3: ( dom (p2 + p1)) = (( dom p2) /\ ( dom p1)) by Lm9;

        

         A4: ( rng p1) c= KK by FINSEQ_1:def 4;

        now

          let k be Nat such that

           A5: k in ( dom (p1 + p2));

          k in ( dom p2) by A2, A5, XBOOLE_0:def 4;

          then

           A6: (p2 . k) in ( rng p2) by FUNCT_1:def 3;

          k in ( dom p1) by A2, A5, XBOOLE_0:def 4;

          then (p1 . k) in ( rng p1) by FUNCT_1:def 3;

          then

          reconsider p1k = (p1 . k), p2k = (p2 . k) as Element of K by A4, A1, A6;

          ((p1 + p2) . k) = (p1k + p2k) by A5, FVSUM_1: 17;

          hence ((p1 + p2) . k) = ((p2 + p1) . k) by A2, A3, A5, FVSUM_1: 17;

        end;

        then

         A7: (p1 + p2) = (p2 + p1) by A3, Lm9, FINSEQ_1: 13;

        (( addFinS K) . (p1,p2)) = (p1 + p2) by Def5;

        hence thesis by A7, Def5;

      end;

    end

    registration

      let K be add-associative non empty addLoopStr;

      cluster ( addFinS K) -> associative;

      coherence

      proof

        set aK = ( addFinS K);

        set KK = the carrier of K;

        let p1,p2,p3 be Element of (KK * );

        reconsider p12 = (p1 + p2), p23 = (p2 + p3) as Element of (KK * ) by FINSEQ_1:def 11;

        

         A1: ( rng p1) c= KK by FINSEQ_1:def 4;

        

         A2: ( rng p2) c= KK by FINSEQ_1:def 4;

        

         A3: ( rng p12) c= KK by FINSEQ_1:def 4;

        

         A4: ( rng p3) c= KK by FINSEQ_1:def 4;

        

         A5: ( rng p23) c= KK by FINSEQ_1:def 4;

        

         A6: ( dom p12) = (( dom p1) /\ ( dom p2)) by Lm9;

        

         A7: ( dom p23) = (( dom p2) /\ ( dom p3)) by Lm9;

        

         A8: ( dom (p12 + p3)) = (( dom p12) /\ ( dom p3)) by Lm9;

        

         A9: ( dom (p1 + p23)) = (( dom p1) /\ ( dom p23)) by Lm9;

        then

         A10: ( dom (p12 + p3)) = ( dom (p1 + p23)) by A6, A8, A7, XBOOLE_1: 16;

        now

          let k be Nat such that

           A11: k in ( dom (p12 + p3));

          

           A12: k in ( dom p12) by A8, A11, XBOOLE_0:def 4;

          then

           A13: (p12 . k) in ( rng p12) by FUNCT_1:def 3;

          k in ( dom p1) by A6, A12, XBOOLE_0:def 4;

          then

           A14: (p1 . k) in ( rng p1) by FUNCT_1:def 3;

          

           A15: k in ( dom p3) by A8, A11, XBOOLE_0:def 4;

          then

           A16: (p3 . k) in ( rng p3) by FUNCT_1:def 3;

          

           A17: k in ( dom p2) by A6, A12, XBOOLE_0:def 4;

          then

           A18: (p2 . k) in ( rng p2) by FUNCT_1:def 3;

          

           A19: k in ( dom p23) by A7, A15, A17, XBOOLE_0:def 4;

          then (p23 . k) in ( rng p23) by FUNCT_1:def 3;

          then

          reconsider p1k = (p1 . k), p12k = (p12 . k), p2k = (p2 . k), p23k = (p23 . k), p3k = (p3 . k) as Element of K by A1, A2, A4, A3, A5, A14, A13, A16, A18;

          

           A20: (p12 . k) = (p1k + p2k) by A12, FVSUM_1: 17;

          

           A21: ((p12 + p3) . k) = (p12k + p3k) by A11, FVSUM_1: 17;

          

           A22: (p23 . k) = (p2k + p3k) by A19, FVSUM_1: 17;

          ((p1 + p23) . k) = (p1k + p23k) by A10, A11, FVSUM_1: 17;

          hence ((p1 + p23) . k) = ((p12 + p3) . k) by A20, A22, A21, RLVECT_1:def 3;

        end;

        then

         A23: (p1 + p23) = (p12 + p3) by A6, A8, A7, A9, FINSEQ_1: 13, XBOOLE_1: 16;

        

        thus (aK . (p1,(aK . (p2,p3)))) = (aK . (p1,p23)) by Def5

        .= (p1 + p23) by Def5

        .= (aK . (p12,p3)) by A23, Def5

        .= (aK . ((aK . (p1,p2)),p3)) by Def5;

      end;

    end

    theorem :: MATRIX11:55

    

     Th55: for K be Ring holds for A,B be Matrix of K st ( width A) = ( len B) & ( len B) > 0 holds for i st i in ( Seg ( len A)) holds ex P be FinSequence of (the carrier of K * ) st ( len P) = ( len B) & ( Line ((A * B),i)) = (( addFinS K) "**" P) & for j st j in ( Seg ( len B)) holds (P . j) = ((A * (i,j)) * ( Line (B,j)))

    proof

      let K be Ring;

      let A,B be Matrix of K such that

       A1: ( width A) = ( len B) and

       A2: ( len B) > 0 ;

      set aa = the addF of K;

      set mm = the multF of K;

      set a = ( addFinS K);

      set KK = the carrier of K;

      reconsider m = ( len B), w = ( width B) as Nat;

      let i such that

       A3: i in ( Seg ( len A));

      deffunc F( Nat) = ((A * (i,$1)) * ( Line (B,$1)));

      consider P be FinSequence such that

       A4: ( len P) = ( len B) and

       A5: for k be Nat st k in ( dom P) holds (P . k) = F(k) from FINSEQ_1:sch 2;

      

       A6: ( dom P) = ( dom B) by A4, FINSEQ_3: 29

      .= ( Seg ( len B)) by FINSEQ_1:def 3;

      ( rng P) c= (KK * )

      proof

        let y be object;

        assume y in ( rng P);

        then

        consider x be object such that

         A7: x in ( dom P) and

         A8: y = (P . x) by FUNCT_1:def 3;

        reconsider x as Element of NAT by A7;

        (P . x) = ((A * (i,x)) * ( Line (B,x))) by A5, A7;

        hence thesis by A8, FINSEQ_1:def 11;

      end;

      then

      reconsider P as FinSequence of (KK * ) by FINSEQ_1:def 4;

      

       A9: m >= 1 by A2, NAT_1: 14;

      then

      consider F be sequence of (KK * ) such that

       A10: (F . 1) = (P . 1) and

       A11: for n be Nat st 0 <> n & n < ( len P) holds (F . (n + 1)) = (a . ((F . n),(P . (n + 1)))) and

       A12: (a "**" P) = (F . ( len P)) by A4, FINSOP_1:def 1;

      defpred P[ Nat] means 1 <= $1 & $1 <= m implies for F1 be FinSequence of KK st (F . $1) = F1 holds ( len F1) = w & for j be Element of NAT st j in ( Seg w) holds ex LC be FinSequence of KK st LC = (( mlt (( Line (A,i)),( Col (B,j)))) | ( Seg $1)) & (aa "**" LC) = (F1 . j);

      

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

      proof

        let k be Nat such that

         A14: P[k];

        set k1 = (k + 1);

        assume that

         A15: 1 <= k1 and

         A16: k1 <= m;

        

         A17: k1 in ( Seg m) by A15, A16;

        let Fk1 be FinSequence of KK such that

         A18: (F . k1) = Fk1;

        per cases ;

          suppose

           A19: k = 0 ;

          then

           A20: (P . 1) = ((A * (i,1)) * ( Line (B,1))) by A5, A6, A17;

          

           A21: ( len ( Line (B,1))) = w by MATRIX_0:def 7;

          hence ( len Fk1) = w by A10, A18, A19, A20, Lm5;

          let j be Element of NAT such that

           A22: j in ( Seg w);

          ( len Fk1) = w by A10, A18, A19, A20, A21, Lm5;

          then

           A23: j in ( dom Fk1) by A22, FINSEQ_1:def 3;

          (( Line (B,1)) . j) = (B * (1,j)) by A22, MATRIX_0:def 7;

          then

           A24: (Fk1 . j) = ((A * (i,1)) * (B * (1,j))) by A10, A18, A19, A20, A23, FVSUM_1: 50;

          set C = ( Col (B,j));

          set L = ( Line (A,i));

          reconsider LC1 = (( mlt (L,C)) | ( Seg k1)), mLC = ( mlt (L,C)) as FinSequence of KK by FINSEQ_1: 18;

          

           A25: (mm .: (L,C)) is Element of (m -tuples_on KK) by A1, FINSEQ_2: 120;

          then ( len mLC) = m by CARD_1:def 7;

          then

           A26: ( dom mLC) = ( Seg m) by FINSEQ_1:def 3;

          ( Seg 1) = (( Seg m) /\ ( Seg 1)) by A2, FINSEQ_1: 7, NAT_1: 14;

          then

           A27: ( dom LC1) = ( Seg 1) by A19, A26, RELAT_1: 61;

          then

           A28: ( len LC1) = 1 by FINSEQ_1:def 3;

          1 in ( Seg 1);

          then (LC1 . 1) = (mLC . 1) by A27, FUNCT_1: 47;

          then

           A29: LC1 = <*(mLC . 1)*> by A28, FINSEQ_1: 40;

          take LC1;

          

           A30: 1 in ( Seg m) by A9;

          ( len mLC) = m by A25, CARD_1:def 7;

          then

           A31: 1 in ( dom mLC) by A30, FINSEQ_1:def 3;

          ( Seg m) = ( dom B) by FINSEQ_1:def 3;

          then

           A32: (C . 1) = (B * (1,j)) by A30, MATRIX_0:def 8;

          (L . 1) = (A * (i,1)) by A1, A30, MATRIX_0:def 7;

          then (mLC . 1) = ((A * (i,1)) * (B * (1,j))) by A32, A31, FVSUM_1: 60;

          hence thesis by A24, A29, FINSOP_1: 11;

        end;

          suppose

           A33: k > 0 ;

          ( dom P) = ( Seg m) by A4, FINSEQ_1:def 3;

          then

           A34: (P . k1) in ( rng P) by A17, FUNCT_1:def 3;

          ( rng P) c= (KK * ) by FINSEQ_1:def 4;

          then

          reconsider Pk1 = (P . k1), Fk = (F . k) as FinSequence of KK by A34, FINSEQ_1:def 11;

          reconsider Pk1, Fk as Element of (KK * ) by FINSEQ_1:def 11;

          

           A35: (a . (Fk,Pk1)) = (Fk + Pk1) by Def5;

          

           A36: (k + 0 ) < k1 by XREAL_1: 8;

          then k < m by A16, XXREAL_0: 2;

          then

           A37: Fk1 = (Fk + Pk1) by A4, A11, A18, A33, A35;

          

           A38: ( len ( Line (B,k1))) = w by MATRIX_0:def 7;

          Pk1 = F(k1) by A5, A6, A17;

          then ( len Pk1) = w by A38, Lm5;

          then

           A39: ( dom Pk1) = ( Seg w) by FINSEQ_1:def 3;

          

           A40: w in NAT by ORDINAL1:def 12;

          

           A41: ( len Fk) = w by A14, A16, A33, A36, NAT_1: 14, XXREAL_0: 2;

          then ( dom Fk) = ( Seg w) by FINSEQ_1:def 3;

          then

           A42: ( dom (Fk + Pk1)) = (( Seg w) /\ ( Seg w)) by A39, Lm9;

          hence ( len Fk1) = w by A37, FINSEQ_1:def 3, A40;

          

           A43: ( rng Fk) c= KK by FINSEQ_1:def 4;

          set L = ( Line (A,i));

          

           A44: Pk1 = F(k1) by A5, A6, A17;

          let j be Element of NAT such that

           A45: j in ( Seg w);

          

           A46: (( Line (B,k1)) . j) = (B * (k1,j)) by A45, MATRIX_0:def 7;

          then (Pk1 . j) = ((A * (i,k1)) * (B * (k1,j))) by A39, A45, A44, FVSUM_1: 50;

          then

          reconsider Pk1j = (Pk1 . j) as Element of KK;

          set C = ( Col (B,j));

          consider LC be FinSequence of KK such that

           A47: LC = (( mlt (L,C)) | ( Seg k)) and

           A48: (the addF of K "**" LC) = (Fk . j) by A14, A16, A33, A36, A45, NAT_1: 14, XXREAL_0: 2;

          reconsider LC1 = (( mlt (L,C)) | ( Seg k1)), mLC = ( mlt (L,C)) as FinSequence of KK by FINSEQ_1: 18;

          take LC1;

          (mm .: (L,C)) is Element of (m -tuples_on KK) by A1, FINSEQ_2: 120;

          then ( len mLC) = m by CARD_1:def 7;

          then

           A49: k1 in ( dom mLC) by A17, FINSEQ_1:def 3;

          

           A50: k1 in ( Seg m) by A15, A16;

          then

           A51: (L . k1) = (A * (i,k1)) by A1, MATRIX_0:def 7;

          ( Seg m) = ( dom B) by FINSEQ_1:def 3;

          then (C . k1) = (B * (k1,j)) by A50, MATRIX_0:def 8;

          then

           A52: (mLC . k1) = ((A * (i,k1)) * (B * (k1,j))) by A51, A49, FVSUM_1: 60;

          LC1 = (LC ^ <*(mLC . k1)*>) by A47, A49, FINSEQ_5: 10;

          then

           A53: (aa "**" LC1) = (aa . ((Fk . j),((A * (i,k1)) * (B * (k1,j))))) by A48, A52, FINSOP_1: 4, FVSUM_1: 8;

          j in ( dom Fk) by A41, A45, FINSEQ_1:def 3;

          then (Fk . j) in ( rng Fk) by FUNCT_1:def 3;

          then

          reconsider Fkj = (Fk . j) as Element of KK by A43;

          (Fk1 . j) = (Fkj + Pk1j) by A42, A37, A45, FVSUM_1: 17;

          hence thesis by A39, A45, A46, A44, A53, FVSUM_1: 50;

        end;

      end;

      set L = ( Line ((A * B),i));

      ( width (A * B)) = w by A1, MATRIX_3:def 4;

      then

       A54: ( len L) = w by MATRIX_0:def 7;

      reconsider Fm = (F . m) as FinSequence of KK;

      

       A55: P[ 0 ];

      

       A56: for k be Nat holds P[k] from NAT_1:sch 2( A55, A13);

      

       A57: for j be Nat st 1 <= j & j <= ( len L) holds (L . j) = (Fm . j)

      proof

        set AB = (A * B);

        set LA = ( Line (A,i));

        let j be Nat such that

         A58: 1 <= j and

         A59: j <= ( len L);

        set CB = ( Col (B,j));

        (mm .: (LA,CB)) is Element of (m -tuples_on KK) by A1, FINSEQ_2: 120;

        then ( len ( mlt (LA,CB))) = m by CARD_1:def 7;

        then

         A60: ( dom ( mlt (LA,CB))) = ( Seg m) by FINSEQ_1:def 3;

        

         A61: j in ( Seg w) by A54, A58, A59;

        then ex LC be FinSequence of KK st LC = (( mlt (LA,CB)) | ( Seg m)) & (aa "**" LC) = (Fm . j) by A9, A56;

        then

         A62: (Fm . j) = (LA "*" CB) by A60;

        

         A63: ( len AB) = ( len A) by A1, MATRIX_3:def 4;

        

         A64: ( width AB) = w by A1, MATRIX_3:def 4;

        ( len A) <> 0 by A3;

        then AB is Matrix of ( len A), w, K by A63, A64, MATRIX_0: 20;

        then ( Indices AB) = [:( Seg ( len A)), ( Seg w):] by A64, MATRIX_0: 25;

        then [i, j] in ( Indices AB) by A3, A61, ZFMISC_1: 87;

        then (AB * (i,j)) = (LA "*" CB) by A1, MATRIX_3:def 4;

        hence thesis by A61, A62, A64, MATRIX_0:def 7;

      end;

      take P;

      thus ( len P) = ( len B) by A4;

      ( len Fm) = w by A9, A56;

      hence L = (a "**" P) by A4, A12, A54, A57;

      let j;

      assume j in ( Seg ( len B));

      hence thesis by A5, A6;

    end;

    theorem :: MATRIX11:56

    

     Th56: for A,B,C be Matrix of n, K, i st i in ( Seg n) holds ex P be FinSequence of K st ( len P) = n & ( Det ( RLine (C,i,( Line ((A * B),i))))) = (the addF of K "**" P) & for j st j in ( Seg n) holds (P . j) = ((A * (i,j)) * ( Det ( RLine (C,i,( Line (B,j))))))

    proof

      let A,B,C be Matrix of n, K, i such that

       A1: i in ( Seg n);

      ( Seg n) <> {} by A1;

      then

       A2: n <> 0 ;

      set a = ( addFinS K);

      

       A3: ( len B) = n by MATRIX_0: 24;

      deffunc F( Nat) = ((A * (i,$1)) * ( Det ( RLine (C,i,( Line (B,$1))))));

      set aa = the addF of K;

      set KK = the carrier of K;

      

       A4: ( len A) = n by MATRIX_0: 24;

      consider D be FinSequence of KK such that

       A5: ( len D) = ( len A) and

       A6: for j be Nat st j in ( dom D) holds (D . j) = F(j) from FINSEQ_2:sch 1;

      

       A7: n <> 0 by A1;

      then ( len D) >= 1 by A4, A5, NAT_1: 14;

      then

      consider Fd be sequence of KK such that

       A8: (Fd . 1) = (D . 1) and

       A9: for k be Nat st 0 <> k & k < n holds (Fd . (k + 1)) = (aa . ((Fd . k),(D . (k + 1)))) and

       A10: (aa "**" D) = (Fd . n) by A4, A5, FINSOP_1:def 1;

      

       A11: ( dom D) = ( Seg ( len A)) by A5, FINSEQ_1:def 3;

      ( width A) = n by MATRIX_0: 24;

      then

      consider P be FinSequence of (KK * ) such that

       A12: ( len P) = n and

       A13: ( Line ((A * B),i)) = (a "**" P) and

       A14: for j st j in ( Seg ( len B)) holds (P . j) = ((A * (i,j)) * ( Line (B,j))) by A1, A7, A3, A4, Th55;

      ( len P) >= 1 by A12, A2, NAT_1: 14;

      then

      consider Fp be sequence of (KK * ) such that

       A15: (Fp . 1) = (P . 1) and

       A16: for k be Nat st 0 <> k & k < n holds (Fp . (k + 1)) = (a . ((Fp . k),(P . (k + 1)))) and

       A17: ( Line ((A * B),i)) = (Fp . n) by A12, A13, FINSOP_1:def 1;

      defpred P[ Nat] means 1 <= $1 & $1 <= n implies for pK be FinSequence of K st pK = (Fp . $1) holds ( len pK) = n & (Fd . $1) = ( Det ( RLine (C,i,pK)));

      

       A18: ( width B) = n by MATRIX_0: 24;

      

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

      proof

        let k be Nat such that

         A20: P[k];

        set k1 = (k + 1);

        set A9 = (A * (i,k1));

        set L = ( Line (B,k1));

        assume that

         A21: 1 <= k1 and

         A22: k1 <= n;

        

         A23: k1 in ( Seg n) by A21, A22;

        let Fpk1 be FinSequence of KK such that

         A24: Fpk1 = (Fp . k1);

        per cases ;

          suppose

           A25: k = 0 ;

          

           A26: (P . k1) = (A9 * L) by A3, A14, A23;

          

           A27: ( len L) = n by A18, MATRIX_0:def 7;

          (D . k1) = F() by A4, A6, A11, A23, A25;

          hence thesis by A1, A15, A8, A24, A25, A26, A27, Lm5, Th34;

        end;

          suppose

           A28: k > 0 ;

          k1 in ( dom P) by A12, A23, FINSEQ_1:def 3;

          then

           A29: (P . k1) in ( rng P) by FUNCT_1:def 3;

          ( rng P) c= (KK * ) by FINSEQ_1:def 4;

          then

          reconsider Pk1 = (P . k1), Fpk = (Fp . k) as Element of (KK * ) by A29, FINSEQ_1:def 11;

          

           A30: (k + 0 ) < k1 by XREAL_1: 8;

          then

           A31: (Fd . k) = ( Det ( RLine (C,i,Fpk))) by A20, A22, A28, NAT_1: 14, XXREAL_0: 2;

          

           A32: ( len Fpk) = n by A20, A22, A28, A30, NAT_1: 14, XXREAL_0: 2;

          

           A33: k < n by A22, A30, XXREAL_0: 2;

          then

           A34: (Fd . k1) = (aa . ((Fd . k),(D . k1))) by A9, A28;

          

           A35: (P . k1) = (A9 * L) by A3, A14, A23;

          Fpk1 = (a . (Fpk,Pk1)) by A16, A24, A28, A33;

          then

           A36: Fpk1 = (Fpk + (A9 * L)) by A35, Def5;

          

           A37: ( len L) = n by A18, MATRIX_0:def 7;

          then

           A38: ( len (A9 * L)) = n by Lm5;

          ( Det ( RLine (C,i,(A9 * L)))) = (A9 * ( Det ( RLine (C,i,L)))) by A1, A37, Th34;

          then ( Det ( RLine (C,i,Fpk1))) = (( Det ( RLine (C,i,Fpk))) + (A9 * ( Det ( RLine (C,i,L))))) by A1, A32, A36, A38, Th36;

          hence thesis by A4, A6, A11, A23, A31, A34, A32, A36, A38, Lm6;

        end;

      end;

      take D;

      thus ( len D) = n by A5, MATRIX_0: 24;

      

       A39: P[ 0 ];

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

      then P[( len P)];

      hence thesis by A4, A12, A6, A11, A17, A10, A2, NAT_1: 14;

    end;

    theorem :: MATRIX11:57

    

     Th57: for X be set, Y be non empty set, x st not x in X holds ex BIJECT be Function of [:( Funcs (X,Y)), Y:], ( Funcs ((X \/ {x}),Y)) st BIJECT is bijective & for f be Function of X, Y, F be Function of (X \/ {x}), Y st (F | X) = f holds (BIJECT . (f,(F . x))) = F

    proof

      let X be set, Y be non empty set, x such that

       A1: not x in X;

      set Xx = (X \/ {x});

      set FXY = ( Funcs (X,Y));

      set FXxY = ( Funcs (Xx,Y));

      defpred P[ set, set] means for f be Function of X, Y, F be Function of Xx, Y, y be set st [f, y] = $1 & (F . x) = y & (F | X) = f holds F = $2;

      

       A2: for x be Element of [:FXY, Y:] holds ex y be Element of FXxY st P[x, y]

      proof

        let x9 be Element of [:FXY, Y:];

        consider f,y be object such that

         A3: f in FXY and

         A4: y in Y and

         A5: x9 = [f, y] by ZFMISC_1:def 2;

        reconsider f as Function of X, Y by A3, FUNCT_2: 66;

        (Y \/ {y}) = Y by A4, ZFMISC_1: 40;

        then

        consider F be Function of (X \/ {x}), Y such that

         A6: (F | X) = f and

         A7: (F . x) = y by A1, STIRL2_1: 57;

        reconsider F9 = F as Element of FXxY by FUNCT_2: 8;

        take F9;

        let g be Function of X, Y, G be Function of Xx, Y, y9 be set such that

         A8: [g, y9] = x9 and

         A9: (G . x) = y9 and

         A10: (G | X) = g;

        now

          let xx be object;

          assume xx in Xx;

          then

           A11: xx in X or xx in {x} by XBOOLE_0:def 3;

          

           A12: ( dom f) = X by FUNCT_2:def 1;

          ( dom g) = X by FUNCT_2:def 1;

          then (G . xx) = (g . xx) & (F . xx) = (f . xx) or xx = x by A6, A10, A11, A12, FUNCT_1: 47, TARSKI:def 1;

          hence (G . xx) = (F . xx) by A5, A7, A8, A9, XTUPLE_0: 1;

        end;

        hence thesis by FUNCT_2: 12;

      end;

      consider H be Function of [:FXY, Y:], FXxY such that

       A13: for x be Element of [:FXY, Y:] holds P[x, (H . x)] from FUNCT_2:sch 3( A2);

       A14:

      now

        let x1,x2 be object such that

         A15: x1 in [:FXY, Y:] and

         A16: x2 in [:FXY, Y:] and

         A17: (H . x1) = (H . x2);

        consider f2,y2 be object such that

         A18: f2 in FXY and

         A19: y2 in Y and

         A20: x2 = [f2, y2] by A16, ZFMISC_1:def 2;

        consider f1,y1 be object such that

         A21: f1 in FXY and

         A22: y1 in Y and

         A23: x1 = [f1, y1] by A15, ZFMISC_1:def 2;

        reconsider f1, f2 as Function of X, Y by A21, A18, FUNCT_2: 66;

        (Y \/ {y2}) = Y by A19, ZFMISC_1: 40;

        then

        consider F2 be Function of (X \/ {x}), Y such that

         A24: (F2 | X) = f2 and

         A25: (F2 . x) = y2 by A1, STIRL2_1: 57;

        

         A26: (H . x2) = F2 by A13, A16, A20, A24, A25;

        (Y \/ {y1}) = Y by A22, ZFMISC_1: 40;

        then

        consider F1 be Function of (X \/ {x}), Y such that

         A27: (F1 | X) = f1 and

         A28: (F1 . x) = y1 by A1, STIRL2_1: 57;

        (H . x1) = F1 by A13, A15, A23, A27, A28;

        hence x1 = x2 by A17, A23, A20, A27, A28, A24, A25, A26;

      end;

      take H;

      x in {x} by TARSKI:def 1;

      then

       A29: x in Xx by XBOOLE_0:def 3;

      

       A30: FXxY c= ( rng H)

      proof

        let f9 be object;

        assume f9 in FXxY;

        then

        reconsider f = f9 as Function of Xx, Y by FUNCT_2: 66;

        ( dom f) = Xx by FUNCT_2:def 1;

        then

         A31: ( dom (f | X)) = X by RELAT_1: 62, XBOOLE_1: 7;

        ( rng (f | X)) c= Y by RELAT_1:def 19;

        then

        reconsider fX = (f | X) as Function of X, Y by A31, FUNCT_2: 2;

        

         A32: fX in FXY by FUNCT_2: 8;

        x in {x} by TARSKI:def 1;

        then

         A33: x in Xx by XBOOLE_0:def 3;

        Xx = ( dom f) by FUNCT_2:def 1;

        then

         A34: (f . x) in ( rng f) by A33, FUNCT_1:def 3;

        ( rng f) c= Y by RELAT_1:def 19;

        then

         A35: [fX, (f . x)] in [:FXY, Y:] by A34, A32, ZFMISC_1: 87;

         [:FXY, Y:] = ( dom H) by FUNCT_2:def 1;

        then (H . [fX, (f . x)]) in ( rng H) by A35, FUNCT_1:def 3;

        hence thesis by A13, A35;

      end;

      ( rng H) c= FXxY by RELAT_1:def 19;

      then FXxY = ( rng H) by A30;

      then H is one-to-one onto by A14, FUNCT_2: 19, FUNCT_2:def 3;

      hence H is bijective;

      let f be Function of X, Y, F be Function of (X \/ {x}), Y such that

       A36: (F | X) = f;

      Xx = ( dom F) by FUNCT_2:def 1;

      then

       A37: (F . x) in ( rng F) by A29, FUNCT_1:def 3;

      

       A38: f in FXY by FUNCT_2: 8;

      ( rng F) c= Y by RELAT_1:def 19;

      then [f, (F . x)] in [:FXY, Y:] by A37, A38, ZFMISC_1: 87;

      hence thesis by A13, A36;

    end;

    theorem :: MATRIX11:58

    

     Th58: for X be finite set, Y be non empty finite set, x st not x in X holds for F be BinOp of D st F is having_a_unity & F is commutative & F is associative holds for f be Function of ( Funcs (X,Y)), D holds for g be Function of ( Funcs ((X \/ {x}),Y)), D st for H be Function of X, Y, SF be Element of ( Fin ( Funcs ((X \/ {x}),Y))) st SF = { h where h be Function of (X \/ {x}), Y : (h | X) = H } holds (F $$ (SF,g)) = (f . H) holds (F $$ (( In (( Funcs (X,Y)),( Fin ( Funcs (X,Y))))),f)) = (F $$ (( In (( Funcs ((X \/ {x}),Y)),( Fin ( Funcs ((X \/ {x}),Y))))),g))

    proof

      let X be finite set, Y be non empty finite set, x such that

       A1: not x in X;

      set Xx = (X \/ {x});

      set FXY = ( Funcs (X,Y));

      set FXxY = ( Funcs (Xx,Y));

      consider B be Function of [:FXY, Y:], FXxY such that

       A2: B is bijective and

       A3: for f be Function of X, Y, F be Function of Xx, Y st (F | X) = f holds (B . (f,(F . x))) = F by A1, Th57;

      ( dom B) = [:FXY, Y:] by FUNCT_2:def 1;

      then

      reconsider domB = ( dom B) as Element of ( Fin [:FXY, Y:]) by FINSUB_1:def 5;

      reconsider FXY9 = FXY as Element of ( Fin FXY) by FINSUB_1:def 5;

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

      then

       A5: ( In (FXxY,( Fin FXxY))) = FXxY by SUBSET_1:def 8;

      reconsider Y9 = Y as Element of ( Fin Y) by FINSUB_1:def 5;

      let F be BinOp of D such that

       A6: F is having_a_unity and

       A7: F is commutative and

       A8: F is associative;

      let f be Function of FXY, D;

      let g be Function of FXxY, D such that

       A9: for H be Function of X, Y, SF be Element of ( Fin FXxY) st SF = { h where h be Function of Xx, Y : (h | X) = H } holds (F $$ (SF,g)) = (f . H);

      reconsider gB = (g * B) as Function of [:FXY, Y:], D;

      for z be Element of FXY holds (f . z) = (F $$ (Y9,(( curry gB) . z)))

      proof

        let z be Element of FXY;

        reconsider Z = z as Function of X, Y;

        set SF = { h where h be Function of Xx, Y : (h | X) = Z };

        deffunc Q( object) = [z, $1];

        consider q be Function such that

         A10: ( dom q) = Y & for x be object st x in Y holds (q . x) = Q(x) from FUNCT_1:sch 3;

        

         A11: {z} c= FXY by ZFMISC_1: 31;

        then [: {Z}, Y:] c= [:FXY, Y:] by ZFMISC_1: 95;

        then

        reconsider ZY = [: {Z}, Y:] as Element of ( Fin [:FXY, Y:]) by FINSUB_1:def 5;

        for x9 be object holds x9 in ZY iff x9 in (q .: Y)

        proof

          let x9 be object;

          thus x9 in ZY implies x9 in (q .: Y)

          proof

            assume x9 in ZY;

            then

            consider z9,y9 be object such that

             A12: z9 in {Z} and

             A13: y9 in Y and

             A14: x9 = [z9, y9] by ZFMISC_1:def 2;

            

             A15: z = z9 by A12, TARSKI:def 1;

            (q . y9) = [z, y9] by A10, A13;

            hence thesis by A10, A13, A14, A15, FUNCT_1:def 6;

          end;

          assume x9 in (q .: Y);

          then

          consider y9 be object such that

           A16: y9 in ( dom q) and

           A17: y9 in Y and

           A18: x9 = (q . y9) by FUNCT_1:def 6;

          x9 = [z, y9] by A10, A16, A18;

          hence thesis by A17, ZFMISC_1: 105;

        end;

        then

         A19: (q .: Y) = ZY by TARSKI: 2;

        then

         A20: ( rng q) = ZY by A10, RELAT_1: 113;

        now

          let x1,x2 be object such that

           A21: x1 in ( dom q) and

           A22: x2 in ( dom q) and

           A23: (q . x1) = (q . x2);

          

           A24: (q . x2) = [z, x2] by A10, A22;

           [z, x1] = (q . x1) by A10, A21;

          hence x1 = x2 by A23, A24, XTUPLE_0: 1;

        end;

        then

         A25: q is one-to-one by FUNCT_1:def 4;

        ZY c= [:FXY, Y:] by A11, ZFMISC_1: 95;

        then

        reconsider q as Function of Y, [:FXY, Y:] by A10, A20, FUNCT_2: 2;

        reconsider gBq = (gB * q) as Function of Y, D;

        ( dom gB) = [:FXY, Y:] by FUNCT_2:def 1;

        then

        consider C be Function such that

         A26: (( curry gB) . z) = C and ( dom C) = Y and ( rng C) c= ( rng gB) and

         A27: for y9 be object st y9 in Y holds (C . y9) = (gB . (z,y9)) by FUNCT_5: 29;

        reconsider C as Function of Y, D by A26;

        now

          let x9 be object such that

           A28: x9 in Y;

          

           A29: (q . x9) = [z, x9] by A10, A28;

          (C . x9) = (gB . (z,x9)) by A27, A28;

          hence (C . x9) = (gBq . x9) by A28, A29, FUNCT_2: 15;

        end;

        then

         A30: C = gBq by FUNCT_2: 12;

        

         A31: (B .: ZY) c= SF

        proof

          let b be object;

          assume b in (B .: ZY);

          then

          consider zy be object such that zy in ( dom B) and

           A32: zy in ZY and

           A33: b = (B . zy) by FUNCT_1:def 6;

          consider z9,y9 be object such that

           A34: z9 in {Z} and

           A35: y9 in Y and

           A36: zy = [z9, y9] by A32, ZFMISC_1:def 2;

          (Y \/ {y9}) = Y by A35, ZFMISC_1: 40;

          then

          consider F1 be Function of Xx, Y such that

           A37: (F1 | X) = Z and

           A38: (F1 . x) = y9 by A1, STIRL2_1: 57;

          z9 = Z by A34, TARSKI:def 1;

          then (B . (z9,y9)) = F1 by A3, A37, A38;

          hence thesis by A33, A36, A37;

        end;

        

         A39: SF c= (B .: ZY)

        proof

          x in {x} by TARSKI:def 1;

          then

           A40: x in Xx by XBOOLE_0:def 3;

          let sf be object;

          assume sf in SF;

          then

          consider h be Function of Xx, Y such that

           A41: h = sf and

           A42: (h | X) = Z;

          

           A43: [:FXY, Y:] = ( dom B) by FUNCT_2:def 1;

          ( dom h) = Xx by FUNCT_2:def 1;

          then

           A44: (h . x) in ( rng h) by A40, FUNCT_1:def 3;

          

           A45: ( rng h) c= Y by RELAT_1:def 19;

          then

           A46: [z, (h . x)] in [:FXY, Y:] by A44, ZFMISC_1: 87;

          z in {Z} by TARSKI:def 1;

          then [z, (h . x)] in ZY by A44, A45, ZFMISC_1: 87;

          then (B . (z,(h . x))) in (B .: ZY) by A46, A43, FUNCT_1:def 6;

          hence thesis by A3, A41, A42;

        end;

        then

        reconsider SF as Element of ( Fin FXxY) by A31, XBOOLE_0:def 10;

        (B .: ZY) = SF by A31, A39;

        then

         A47: (F $$ ((B .: ZY),g)) = (f . Z) by A9;

        (F $$ ((B .: ZY),g)) = (F $$ (ZY,gB)) by A7, A8, A2, SETWOP_2: 6;

        hence thesis by A7, A8, A47, A25, A19, A26, A30, SETWOP_2: 6;

      end;

      then (F $$ ( [:FXY9, Y9:],gB)) = (F $$ (FXY9,f)) by A6, A7, A8, MATRIX_3: 30;

      then

       A48: (F $$ (domB,gB)) = (F $$ (FXY9,f)) by FUNCT_2:def 1;

      

       A49: ( rng B) = FXxY by A2, FUNCT_2:def 3;

      (F $$ ((B .: domB),g)) = (F $$ (domB,(g * B))) by A7, A8, A2, SETWOP_2: 6;

      then (F $$ (( In (FXxY,( Fin FXxY))),g)) = (F $$ (domB,(g * B))) by A49, A5, RELAT_1: 113;

      hence thesis by A48;

    end;

    theorem :: MATRIX11:59

    

     Th59: for A,B be Matrix of n, m, D, i st i <= n & 0 < n holds for F be Function of ( Seg i), ( Seg n) holds ex M be Matrix of n, m, D st M = (A +* ((B * (( idseq n) +* F)) | ( Seg i))) & for j holds (j in ( Seg i) implies (M . j) = (B . (F . j))) & ( not j in ( Seg i) implies (M . j) = (A . j))

    proof

      let A,B be Matrix of n, m, D, i such that

       A1: i <= n and

       A2: 0 < n;

      set I = ( idseq n);

      let F be Function of ( Seg i), ( Seg n);

      set IF = (I +* F);

      

       A3: ( dom I) = ( Seg n);

      

       A4: ( rng I) = ( Seg n);

      ( rng F) c= ( Seg n) by RELAT_1:def 19;

      then (( rng F) \/ ( Seg n)) = ( Seg n) by XBOOLE_1: 12;

      then

       A5: ( rng IF) c= ( Seg n) by A4, FUNCT_4: 17;

      

       A6: ( Seg i) c= ( Seg n) by A1, FINSEQ_1: 5;

      then

       A7: (( Seg i) \/ ( Seg n)) = ( Seg n) by XBOOLE_1: 12;

      

       A8: ( dom F) = ( Seg i) by A2, FUNCT_2:def 1;

      then ( dom F) c= ( Seg n) by A1, FINSEQ_1: 5;

      then (( dom F) \/ ( Seg n)) = ( Seg n) by XBOOLE_1: 12;

      then ( dom IF) = ( Seg n) by A3, FUNCT_4:def 1;

      then

      reconsider IF as Function of ( Seg n), ( Seg n) by A5, FUNCT_2: 2;

      reconsider BIF = (B * IF) as Matrix of n, m, D;

      set BIFi = (BIF | ( Seg i));

      set M = (A +* BIFi);

      

       A9: ( len B) = n by A2, MATRIX_0: 23;

      ( len BIF) = ( len B) by Def4;

      then ( dom BIF) = ( Seg n) by A9, FINSEQ_1:def 3;

      then

       A10: ( dom BIFi) = ( Seg i) by A6, RELAT_1: 62;

      ( len A) = n by A2, MATRIX_0: 23;

      then ( dom A) = ( Seg n) by FINSEQ_1:def 3;

      then

       A11: ( dom M) = (( Seg i) \/ ( Seg n)) by A10, FUNCT_4:def 1;

      then

      reconsider M as FinSequence by A7, FINSEQ_1:def 2;

      

       A12: for j holds (j in ( Seg i) implies (M . j) = (B . (F . j))) & ( not j in ( Seg i) implies (M . j) = (A . j))

      proof

        let j;

        thus j in ( Seg i) implies (M . j) = (B . (F . j))

        proof

          

           A13: ( Seg i) c= ( Seg n) by A1, FINSEQ_1: 5;

          assume

           A14: j in ( Seg i);

          then

           A15: (BIFi . j) = (BIF . j) by A10, FUNCT_1: 47;

          (IF . j) = (F . j) by A8, A14, FUNCT_4: 13;

          then

           A16: ( Line (BIF,j)) = (B . (F . j)) by A14, A13, Th38;

          ( Line (BIF,j)) = (BIF . j) by A14, A13, MATRIX_0: 52;

          hence thesis by A10, A14, A16, A15, FUNCT_4: 13;

        end;

        assume not j in ( Seg i);

        hence thesis by A10, FUNCT_4: 11;

      end;

      

       A17: for x st x in ( rng M) holds ex p be FinSequence of D st x = p & ( len p) = m

      proof

        let x;

        assume x in ( rng M);

        then

        consider k be object such that

         A18: k in ( dom M) and

         A19: (M . k) = x by FUNCT_1:def 3;

        reconsider k as Nat by A18;

        per cases ;

          suppose

           A20: k in ( Seg i);

          

           A21: ( rng F) c= ( Seg n) by RELAT_1:def 19;

          

           A22: (F . k) in ( rng F) by A8, A20, FUNCT_1:def 3;

          then

          reconsider Fk = (F . k) as Element of NAT by A21, TARSKI:def 3;

          take L = ( Line (B,Fk));

          

           A23: ( len L) = ( width B) by MATRIX_0:def 7;

          (B . (F . k)) = L by A22, A21, MATRIX_0: 52;

          hence thesis by A2, A12, A19, A20, A23, MATRIX_0: 23;

        end;

          suppose

           A24: not k in ( Seg i);

          take L = ( Line (A,k));

          

           A25: ( len L) = ( width A) by MATRIX_0:def 7;

          (M . k) = (A . k) by A12, A24;

          hence thesis by A2, A11, A7, A18, A19, A25, MATRIX_0: 23, MATRIX_0: 52;

        end;

      end;

      then

      reconsider M as Matrix of D by MATRIX_0: 9;

      n is Element of NAT by ORDINAL1:def 12;

      then

       A26: ( len M) = n by A11, A7, FINSEQ_1:def 3;

      now

        let p be FinSequence of D;

        assume p in ( rng M);

        then ex q be FinSequence of D st p = q & ( len q) = m by A17;

        hence ( len p) = m;

      end;

      then

      reconsider M as Matrix of n, m, D by A26, MATRIX_0:def 2;

      take M;

      thus thesis by A12;

    end;

    

     Lm10: for K be Ring holds for A,B be Matrix of n, n, K, i st i <= n & 0 < n holds ex P be Function of ( Funcs (( Seg i),( Seg n))), the carrier of K st for F be Function of ( Seg i), ( Seg n) holds for M be Matrix of n, n, K st M = ((A * B) +* ((B * (( idseq n) +* F)) | ( Seg i))) & for j holds (j in ( Seg i) implies (M . j) = (B . (F . j))) & ( not j in ( Seg i) implies (M . j) = ((A * B) . j)) holds ex Path be FinSequence of K st ( len Path) = i & (for Fj,j be Nat st j in ( Seg i) & Fj = (F . j) holds (Path . j) = (A * (j,Fj))) & (P . F) = ((the multF of K $$ Path) * ( Det M))

    proof

      let K be Ring;

      let A,B be Matrix of n, n, K, i such that

       A1: i <= n and

       A2: 0 < n;

      set KK = the carrier of K;

      set I = ( idseq n);

      set Sn = ( Seg n);

      set Si = ( Seg i);

      set mm = the multF of K;

      set FF = ( Funcs (Si,Sn));

      reconsider Sn as non empty set by A2;

      set AB = (A * B);

      reconsider AB as Matrix of n, K;

      defpred PP[ object, object] means for F be Function of ( Seg i), ( Seg n) st F = $1 holds for M be Matrix of n, n, K st M = ((A * B) +* ((B * (I +* F)) | Si)) & for j holds (j in Si implies (M . j) = (B . (F . j))) & ( not j in Si implies (M . j) = ((A * B) . j)) holds ex Path be FinSequence of K st ( len Path) = i & (for Fj,j be Nat st j in Si & Fj = (F . j) holds (Path . j) = (A * (j,Fj))) & $2 = ((mm $$ Path) * ( Det M));

      ex f be Function st ( dom f) = Si & ( rng f) c= Sn by FUNCT_1: 8;

      then

      reconsider FF as non empty set;

      

       A3: for x be Element of FF holds ex y be Element of KK st PP[x, y]

      proof

        let x be Element of FF;

        reconsider F = x as Function of Si, Sn by FUNCT_2: 66;

        defpred Path[ object, object] means for Fj,j be Nat st j = $1 & Fj = (F . j) holds $2 = (A * (j,Fj));

        

         A4: i is Element of NAT by ORDINAL1:def 12;

        

         A5: for x9 be object st x9 in Si holds ex y be object st y in KK & Path[x9, y]

        proof

          let x9 be object such that

           A6: x9 in Si;

          reconsider i = x9 as Nat by A6;

          

           A7: ( rng F) c= ( Seg n) by RELAT_1:def 19;

          Si = ( dom F) by FUNCT_2:def 1;

          then (F . i) in ( rng F) by A6, FUNCT_1:def 3;

          then (F . i) in Sn by A7;

          then

          reconsider Fi = (F . i) as Nat;

          take (A * (i,Fi));

          thus thesis;

        end;

        consider path be Function of Si, KK such that

         A8: for x be object st x in Si holds Path[x, (path . x)] from FUNCT_2:sch 1( A5);

        ( dom path) = Si by FUNCT_2:def 1;

        then

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

        ( rng path) c= KK by RELAT_1:def 19;

        then

        reconsider p as FinSequence of K by FINSEQ_1:def 4;

        consider M be Matrix of n, K such that M = (AB +* ((B * (I +* F)) | Si)) and

         A9: for j holds (j in Si implies (M . j) = (B . (F . j))) & ( not j in Si implies (M . j) = (AB . j)) by A1, A2, Th59;

        take ((mm $$ p) * ( Det M));

        let F9 be Function of Si, ( Seg n) such that

         A10: F9 = x;

        let M9 be Matrix of n, n, K such that M9 = ((A * B) +* ((B * (I +* F9)) | Si)) and

         A11: for j holds (j in ( Seg i) implies (M9 . j) = (B . (F9 . j))) & ( not j in ( Seg i) implies (M9 . j) = ((A * B) . j));

        take p;

        ( dom path) = Si by FUNCT_2:def 1;

        hence ( len p) = i & for Fj,j be Nat st j in Si & Fj = (F9 . j) holds (p . j) = (A * (j,Fj)) by A8, A10, A4, FINSEQ_1:def 3;

        

         A12: ( len M9) = n by MATRIX_0: 24;

         A13:

        now

          let k be Nat such that 1 <= k and k <= ( len M);

          per cases ;

            suppose

             A14: k in Si;

            then (M . k) = (B . (F . k)) by A9;

            hence (M . k) = (M9 . k) by A10, A11, A14;

          end;

            suppose

             A15: not k in Si;

            then (M . k) = (AB . k) by A9;

            hence (M . k) = (M9 . k) by A11, A15;

          end;

        end;

        ( len M) = n by MATRIX_0: 24;

        hence thesis by A12, A13, FINSEQ_1: 14;

      end;

      consider P be Function of FF, KK such that

       A16: for x be Element of FF holds PP[x, (P . x)] from FUNCT_2:sch 3( A3);

      reconsider P as Function of ( Funcs (Si,( Seg n))), KK;

      take P;

      let F be Function of Si, ( Seg n);

      reconsider F9 = F as Function of Si, Sn;

      let M be Matrix of n, K such that

       A17: M = ((A * B) +* ((B * (I +* F)) | Si)) and

       A18: for j holds (j in Si implies (M . j) = (B . (F . j))) & ( not j in Si implies (M . j) = ((A * B) . j));

      F9 in FF by FUNCT_2: 8;

      hence thesis by A16, A17, A18;

    end;

    theorem :: MATRIX11:60

    

     Th60: for A,B be Matrix of n, K st 0 < n holds ex P be Function of ( Funcs (( Seg n),( Seg n))), the carrier of K st (for F be Function of ( Seg n), ( Seg n) holds ex Path be FinSequence of K st ( len Path) = n & (for Fj,j be Nat st j in ( Seg n) & Fj = (F . j) holds (Path . j) = (A * (j,Fj))) & (P . F) = ((the multF of K $$ Path) * ( Det (B * F)))) & ( Det (A * B)) = (the addF of K $$ (( In (( Funcs (( Seg n),( Seg n))),( Fin ( Funcs (( Seg n),( Seg n)))))),P))

    proof

      let A,B be Matrix of n, K such that

       A1: 0 < n;

      set AB = (A * B);

      set aa = the addF of K;

      set I = ( idseq n);

      set mm = the multF of K;

      set KK = the carrier of K;

      defpred FF[ Function, Nat] means for F be Function of ( Seg $2), ( Seg n) holds for M be Matrix of n, n, K st M = ((A * B) +* ((B * (I +* F)) | ( Seg $2))) & for j holds (j in ( Seg $2) implies (M . j) = (B . (F . j))) & ( not j in ( Seg $2) implies (M . j) = ((A * B) . j)) holds ex Path be FinSequence of K st ( len Path) = $2 & (for Fj,j be Nat st j in ( Seg $2) & Fj = (F . j) holds (Path . j) = (A * (j,Fj))) & ($1 . F) = ((mm $$ Path) * ( Det M));

      defpred P[ Nat] means $1 <= n implies for FUNC be non empty set st FUNC = ( Funcs (( Seg $1),( Seg n))) holds ex P be Function of FUNC, KK st FF[P, $1] & ( Det AB) = (aa $$ (( In (FUNC,( Fin FUNC))),P));

      

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

      proof

        set Y = ( Seg n);

        let k be Nat such that

         A3: P[k];

        set X = ( Seg k);

        reconsider FUNC = ( Funcs (( Seg k),( Seg n))) as non empty set by A1;

        set k1 = (k + 1);

        assume

         A4: k1 <= n;

        set Xx = (( Seg k) \/ {k1});

        let FUNC1 be non empty set such that

         A5: FUNC1 = ( Funcs (( Seg k1),( Seg n)));

        consider P1 be Function of FUNC1, KK such that

         A6: FF[P1, k1] by A4, A5, Lm10;

        reconsider FUNC19 = ( Funcs (Xx,Y)) as non empty set by A5, FINSEQ_1: 9;

        

         A7: FUNC1 = ( Funcs (Xx,Y)) by A5, FINSEQ_1: 9;

        then

        reconsider P19 = P1 as Function of FUNC19, KK;

        

         A8: (k + 0 ) <= k1 by XREAL_1: 8;

        then

        consider P be Function of FUNC, KK such that

         A9: FF[P, k] and

         A10: ( Det AB) = (aa $$ (( In (FUNC,( Fin FUNC))),P)) by A3, A4, XXREAL_0: 2;

        

         A11: not k1 in X by FINSEQ_3: 8;

        

         A12: for H be Function of X, Y, SF be Element of ( Fin FUNC19) st SF = { h where h be Function of Xx, Y : (h | X) = H } holds (aa $$ (SF,P19)) = (P . H)

        proof

          reconsider YY = Y as non empty set by A1;

          let H be Function of X, Y, SF be Element of ( Fin FUNC19) such that

           A13: SF = { h where h be Function of Xx, Y : (h | X) = H };

          defpred Q[ object, object] means for h be Function of Xx, Y st (h | X) = H & (h . k1) = $1 holds h = $2;

          

           A14: for y be object st y in YY holds ex f9 be object st f9 in SF & Q[y, f9]

          proof

            let y be object;

            assume y in YY;

            then (Y \/ {y}) = Y by ZFMISC_1: 40;

            then

            consider q be Function of Xx, Y such that

             A15: (q | X) = H and

             A16: (q . k1) = y by A11, STIRL2_1: 57;

            take q;

            thus q in SF by A13, A15;

            let h be Function of Xx, Y such that

             A17: (h | X) = H and

             A18: (h . k1) = y;

            now

              let x be object;

              assume x in Xx;

              then

               A19: x in X or x in {k1} by XBOOLE_0:def 3;

              ( dom H) = X by A1, FUNCT_2:def 1;

              then (q . x) = (H . x) & (h . x) = (H . x) or x = k1 by A15, A17, A19, FUNCT_1: 47, TARSKI:def 1;

              hence (h . x) = (q . x) by A16, A18;

            end;

            hence thesis by FUNCT_2: 12;

          end;

          consider QQ be Function of YY, SF such that

           A20: for y be object st y in YY holds Q[y, (QQ . y)] from FUNCT_2:sch 1( A14);

          

           A21: SF c= ( rng QQ)

          proof

            let y be object;

            k1 in {k1} by TARSKI:def 1;

            then

             A22: k1 in Xx by XBOOLE_0:def 3;

            assume

             A23: y in SF;

            then

            consider h be Function of Xx, Y such that

             A24: y = h and

             A25: (h | X) = H by A13;

            ( dom h) = Xx by A1, FUNCT_2:def 1;

            then

             A26: (h . k1) in ( rng h) by A22, FUNCT_1:def 3;

            

             A27: ( rng h) c= Y by RELAT_1:def 19;

            ( dom QQ) = YY by A23, FUNCT_2:def 1;

            then (QQ . (h . k1)) in ( rng QQ) by A26, A27, FUNCT_1:def 3;

            hence thesis by A20, A24, A25, A26, A27;

          end;

          ( rng QQ) c= SF by RELAT_1:def 19;

          then

           A28: ( rng QQ) = SF by A21;

          (Y \/ {n}) = Y by A1, FINSEQ_1: 3, ZFMISC_1: 40;

          then

          consider h be Function of Xx, Y such that

           A29: (h | X) = H and (h . k1) = n by A11, STIRL2_1: 57;

          

           A30: SF c= FUNC19 by FINSUB_1:def 5;

          k <= n by A4, A8, XXREAL_0: 2;

          then

          consider Mh be Matrix of n, K such that

           A31: Mh = (AB +* ((B * (I +* H)) | ( Seg k))) and

           A32: for j holds (j in ( Seg k) implies (Mh . j) = (B . (H . j))) & ( not j in ( Seg k) implies (Mh . j) = (AB . j)) by A1, Th59;

          consider Path be FinSequence of K such that

           A33: ( len Path) = k and

           A34: for Hj,j be Nat st j in ( Seg k) & Hj = (H . j) holds (Path . j) = (A * (j,Hj)) and

           A35: (P . H) = ((mm $$ Path) * ( Det Mh)) by A9, A31, A32;

          

           A36: (Mh . k1) = (AB . k1) by A11, A32;

          h in SF by A13, A29;

          then

          reconsider QQ as Function of YY, FUNC19 by A28, A30, FUNCT_2: 6;

          

           A37: ( dom (P19 * QQ)) = Y by FUNCT_2:def 1;

          

           A38: (QQ .: ( dom QQ)) = SF by A28, RELAT_1: 113;

          (1 + 0 ) <= k1 by XREAL_1: 7;

          then

           A39: k1 in ( Seg n) by A4;

          then

           A40: (AB . k1) = ( Line (AB,k1)) by MATRIX_0: 52;

          (Mh . k1) = ( Line (Mh,k1)) by A39, MATRIX_0: 52;

          then Mh = ( RLine (Mh,k1,( Line (AB,k1)))) by A36, A40, Th30;

          then

          consider SUM1 be FinSequence of KK such that

           A41: ( len SUM1) = n and

           A42: ( Det Mh) = (aa "**" SUM1) and

           A43: for j st j in Y holds (SUM1 . j) = ((A * (k1,j)) * ( Det ( RLine (Mh,k1,( Line (B,j)))))) by A39, Th56;

          

           A44: ( dom ( id Y)) = Y;

          set PA = (mm "**" Path);

          set PS = (PA * SUM1);

          ( len PS) = n by A41, Lm5;

          then

           A45: ( dom PS) = Y by FINSEQ_1:def 3;

          set PSaa = ( [#] (PS,( the_unity_wrt aa)));

          

           A46: for j be Nat st j in Y holds ((P19 * QQ) . j) = ((PA * (A * (k1,j))) * ( Det ( RLine (Mh,k1,( Line (B,j))))))

          proof

            

             A47: ( width B) = n by MATRIX_0: 24;

            

             A48: ( len Mh) = n by MATRIX_0: 24;

            

             A49: ( dom (P19 * QQ)) = Y by FUNCT_2:def 1;

            

             A50: ( width Mh) = n by MATRIX_0: 24;

            let j be Nat such that

             A51: j in Y;

            (Y \/ {j}) = Y by A51, ZFMISC_1: 40;

            then

            consider hj be Function of Xx, Y such that

             A52: (hj | X) = H and

             A53: (hj . k1) = j by A11, STIRL2_1: 57;

            set L = ( Line (B,j));

            set R = ( RLine (Mh,k1,L));

            Xx = ( Seg k1) by FINSEQ_1: 9;

            then

            reconsider hj9 = hj as Function of ( Seg k1), Y;

            consider Mhj be Matrix of n, K such that

             A54: Mhj = (AB +* ((B * (I +* hj9)) | ( Seg k1))) and

             A55: for i holds (i in ( Seg k1) implies (Mhj . i) = (B . (hj9 . i))) & ( not i in ( Seg k1) implies (Mhj . i) = (AB . i)) by A4, Th59;

            

             A56: ( len Mhj) = n by MATRIX_0: 24;

            

             A57: ( len L) = ( width B) by MATRIX_0:def 7;

             A58:

            now

              

               A59: (k + 0 ) < k1 by XREAL_1: 8;

              let i be Nat such that

               A60: 1 <= i and

               A61: i <= ( len Mhj);

              

               A62: i in ( Seg n) by A56, A60, A61;

              per cases ;

                suppose

                 A63: i <= k;

                then i <= k1 by A59, XXREAL_0: 2;

                then

                 A64: i in ( Seg k1) by A60;

                

                 A65: ( Line (R,i)) = (R . i) by A62, MATRIX_0: 52;

                

                 A66: i in X by A60, A63;

                then

                 A67: (Mh . i) = (B . (H . i)) by A32;

                ( dom H) = X by A56, A60, A61, FUNCT_2:def 1;

                then

                 A68: (H . i) = (hj . i) by A52, A66, FUNCT_1: 47;

                

                 A69: ( Line (Mh,i)) = (Mh . i) by A62, MATRIX_0: 52;

                ( Line (R,i)) = ( Line (Mh,i)) by A62, A59, A63, Th28;

                hence (Mhj . i) = (R . i) by A55, A65, A69, A67, A68, A64;

              end;

                suppose

                 A70: i > k & i <= k1;

                

                 A71: k1 in ( Seg k1) by FINSEQ_1: 4;

                

                 A72: L = (B . j) by A51, MATRIX_0: 52;

                

                 A73: (R . i) = ( Line (R,i)) by A62, MATRIX_0: 52;

                

                 A74: i = k1 by A70, NAT_1: 9;

                then L = ( Line (R,i)) by A57, A47, A50, A62, Th28;

                hence (Mhj . i) = (R . i) by A53, A55, A74, A71, A73, A72;

              end;

                suppose

                 A75: i > k & i > k1;

                then not i in ( Seg k1) by FINSEQ_1: 1;

                then

                 A76: (Mhj . i) = (AB . i) by A55;

                

                 A77: ( Line (R,i)) = (R . i) by A62, MATRIX_0: 52;

                

                 A78: not i in X by A75, FINSEQ_1: 1;

                

                 A79: ( Line (Mh,i)) = (Mh . i) by A62, MATRIX_0: 52;

                ( Line (R,i)) = ( Line (Mh,i)) by A62, A75, Th28;

                hence (Mhj . i) = (R . i) by A32, A77, A79, A78, A76;

              end;

            end;

            ( len R) = ( len Mh) by Lm4;

            then R = Mhj by A48, A56, A58;

            then

            consider Pathj be FinSequence of K such that

             A80: ( len Pathj) = k1 and

             A81: for m,j be Nat st j in ( Seg k1) & m = (hj . j) holds (Pathj . j) = (A * (j,m)) and

             A82: (P1 . hj) = ((mm "**" Pathj) * ( Det R)) by A6, A54, A55;

            

             A83: (Pathj . k1) = (A * (k1,j)) by A53, A81, FINSEQ_1: 4;

             A84:

            now

              

               A85: ( rng H) c= Y by RELAT_1:def 19;

              

               A86: X = ( dom H) by A51, FUNCT_2:def 1;

              let i be Nat such that

               A87: 1 <= i and

               A88: i <= ( len Path);

              

               A89: ((Pathj | k) . i) = (Pathj . i) by A33, A88, FINSEQ_3: 112;

              

               A90: i in X by A33, A87, A88;

              then (H . i) in ( rng H) by A86, FUNCT_1:def 3;

              then (H . i) in Y by A85;

              then

              reconsider Hi = (H . i) as Nat;

              i <= k1 by A8, A33, A88, XXREAL_0: 2;

              then

               A91: i in ( Seg k1) by A87;

              i in X by A33, A87, A88;

              then

               A92: (Path . i) = (A * (i,Hi)) by A34;

              (H . i) = (hj . i) by A52, A90, A86, FUNCT_1: 47;

              hence (Path . i) = ((Pathj | X) . i) by A81, A91, A92, A89;

            end;

            ( len (Pathj | k)) = k by A8, A80, FINSEQ_1: 59;

            then Pathj = (Path ^ <*(Pathj . k1)*>) by A33, A80, A84, FINSEQ_1: 14, FINSEQ_3: 55;

            then

             A93: (mm "**" Pathj) = (PA * (A * (k1,j))) by A83, FINSOP_1: 4;

            (QQ . j) = hj by A20, A51, A52, A53;

            hence thesis by A51, A82, A49, A93, FUNCT_1: 12;

          end;

          now

            let y be object such that

             A94: y in ( dom PS);

            reconsider j = y as Nat by A94;

            (SUM1 . j) = ((A * (k1,j)) * ( Det ( RLine (Mh,k1,( Line (B,j)))))) by A43, A45, A94;

            

            hence (PS . y) = (PA * ((A * (k1,j)) * ( Det ( RLine (Mh,k1,( Line (B,j))))))) by A94, FVSUM_1: 50

            .= ((PA * (A * (k1,j))) * ( Det ( RLine (Mh,k1,( Line (B,j)))))) by GROUP_1:def 3

            .= ((P19 * QQ) . y) by A46, A45, A94;

          end;

          then PS = (P19 * QQ) by A37, A45, FUNCT_1: 2;

          then

           A95: (PSaa | ( dom PS)) = (P19 * QQ) by SETWOP_2: 21;

          now

            let x1,x2 be object such that

             A96: x1 in Y and

             A97: x2 in Y and

             A98: (QQ . x1) = (QQ . x2);

            (Y \/ {x2}) = Y by A97, ZFMISC_1: 40;

            then

             A99: ex h2 be Function of Xx, Y st (h2 | X) = H & (h2 . k1) = x2 by A11, STIRL2_1: 57;

            (Y \/ {x1}) = Y by A96, ZFMISC_1: 40;

            then

            consider h1 be Function of Xx, Y such that

             A100: (h1 | X) = H and

             A101: (h1 . k1) = x1 by A11, STIRL2_1: 57;

            (QQ . x1) = h1 by A20, A96, A100, A101;

            hence x1 = x2 by A20, A97, A98, A101, A99;

          end;

          then

           A102: QQ is one-to-one by FUNCT_2: 19;

          reconsider Y9 = Y as Element of ( Fin YY) by FINSUB_1:def 5;

          

           A103: ( dom QQ) = Y9 by FUNCT_2:def 1;

          

           A104: ( rng ( id Y)) = Y;

          ((P19 * QQ) * ( id Y)) = (P19 * QQ) by A37, RELAT_1: 52;

          

          then (aa $$ (Y9,(P19 * QQ))) = (aa $$ (( findom PS),PSaa)) by A45, A44, A104, A95, SETWOP_2: 5

          .= ( Sum PS) by FVSUM_1: 8, SETWOP_2:def 2

          .= (PA * ( Sum SUM1)) by FVSUM_1: 73

          .= (P . H) by A35, A42;

          hence thesis by A102, A38, A103, SETWOP_2: 6;

        end;

        aa is having_a_unity by FVSUM_1: 8;

        then ( Det AB) = (aa $$ (( In (FUNC19,( Fin FUNC19))),P19)) by A1, A10, A11, A12, Th58;

        hence thesis by A6, A7;

      end;

      set FUN = ( Funcs (( Seg n),( Seg n)));

      

       A105: P[ 0 ]

      proof

        reconsider E = {} as Function of ( Seg 0 ), ( Seg n) by XBOOLE_1: 2;

        assume 0 <= n;

        

         A106: ( the_unity_wrt mm) = ( 1_ K) by GROUP_1: 22;

        let FUNC be non empty set such that

         A107: FUNC = ( Funcs (( Seg 0 ),( Seg n)));

        consider P be Function of FUNC, KK such that

         A108: FF[P, 0 ] by A1, A107, Lm10;

        

         A109: FUNC = {E} by A107, FUNCT_5: 57;

        then

         A110: E in FUNC by TARSKI:def 1;

        FUNC is finite by A109;

        then FUNC in ( Fin FUNC) by FINSUB_1:def 5;

        then ( In (FUNC,( Fin FUNC))) = {E} by SUBSET_1:def 8, A109;

        then

         A111: (aa $$ (( In (FUNC,( Fin FUNC))),P)) = (P . E) by A110, SETWISEO: 17;

        consider M be Matrix of n, K such that

         A112: M = (AB +* ((B * (I +* E)) | ( Seg 0 ) qua set)) and

         A113: for j holds (j in ( Seg 0 ) implies (M . j) = (B . (E . j))) & ( not j in ( Seg 0 ) implies (M . j) = (AB . j)) by A1, Th59;

        

         A114: M = (AB +* {} ) by A112;

        consider Path be FinSequence of K such that

         A115: ( len Path) = 0 and for Fj,j be Nat st j in ( Seg 0 ) & Fj = (E . j) holds (Path . j) = (A * (j,Fj)) and

         A116: (P . E) = ((mm $$ Path) * ( Det M)) by A108, A112, A113;

        Path = ( <*> KK) by A115;

        then (mm "**" Path) = ( 1_ K) by A106, FINSOP_1: 10;

        then (P . E) = ( Det AB) by A116, A114;

        hence thesis by A108, A111;

      end;

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

      then

      consider P be Function of FUN, KK such that

       A117: FF[P, n] and

       A118: ( Det AB) = (aa $$ (( In (FUN,( Fin FUN))),P));

      take P;

      thus for F be Function of ( Seg n), ( Seg n) holds ex Path be FinSequence of K st ( len Path) = n & (for Fj,j be Nat st j in ( Seg n) & Fj = (F . j) holds (Path . j) = (A * (j,Fj))) & (P . F) = ((the multF of K $$ Path) * ( Det (B * F)))

      proof

        ( len AB) = n by MATRIX_0: 24;

        then

         A119: ( dom AB) = ( Seg n) by FINSEQ_1:def 3;

        let F be Function of ( Seg n), ( Seg n);

        

         A120: ( dom I) = ( Seg n);

        ( dom F) = ( Seg n) by FUNCT_2: 52;

        then

         A121: (I +* F) = F by A120, FUNCT_4: 19;

        

         A122: ( len B) = n by MATRIX_0: 24;

        ( len (B * F)) = ( len B) by Def4;

        then

         A123: ( dom (B * F)) = ( Seg n) by A122, FINSEQ_1:def 3;

        consider M be Matrix of n, K such that

         A124: M = (AB +* ((B * (I +* F)) | ( Seg n))) and

         A125: for j holds (j in ( Seg n) implies (M . j) = (B . (F . j))) & ( not j in ( Seg n) implies (M . j) = (AB . j)) by A1, Th59;

        M = (B * F) by A124, A121, A123, A119, FUNCT_4: 19;

        hence thesis by A117, A124, A125;

      end;

      thus thesis by A118;

    end;

    theorem :: MATRIX11:61

    

     Th61: K is non degenerated well-unital domRing-like implies for A,B be Matrix of n, K st 0 < n holds ex P be Function of ( Permutations n), the carrier of K st ( Det (A * B)) = (the addF of K $$ (( In (( Permutations n),( Fin ( Permutations n)))),P)) & for perm be Element of ( Permutations n) holds (P . perm) = ((the multF of K $$ ( Path_matrix (perm,A))) * ( - (( Det B),perm)))

    proof

      assume

       A0: K is non degenerated well-unital domRing-like;

      let A,B be Matrix of n, K such that

       A1: 0 < n;

      set P = ( Permutations n);

      

       A2: ( dom ( id P)) = P;

      set KK = the carrier of K;

      set mm = the multF of K;

      set aa = the addF of K;

      set AB = (A * B);

      set X = ( Seg n);

      set F = ( Funcs (X,X));

      consider SUM1 be Function of F, KK such that

       A3: for F be Function of X, X holds ex Path be FinSequence of K st ( len Path) = n & (for Fj,j be Nat st j in ( Seg n) & Fj = (F . j) holds (Path . j) = (A * (j,Fj))) & (SUM1 . F) = ((mm $$ Path) * ( Det (B * F))) and

       A4: ( Det AB) = (aa $$ (( In (F,( Fin F))),SUM1)) by A1, Th60;

      reconsider FP = (F \ P) as Element of ( Fin F) by FINSUB_1:def 5;

      

       A6: P c= F

      proof

        let x be object;

        assume x in P;

        then

        reconsider p = x as Permutation of X by MATRIX_1:def 12;

        p is Element of F by FUNCT_2: 9;

        hence thesis;

      end;

      then

      reconsider P9 = P as Element of ( Fin F) by FINSUB_1:def 5;

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

      then

       A7: P = ( In (P,( Fin P))) by SUBSET_1:def 8;

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

      then

       A8: ( In (F,( Fin F))) = F by SUBSET_1:def 8;

       A9:

      now

        per cases ;

          suppose FP = {} ;

          then F c= P by XBOOLE_1: 37;

          hence ( Det AB) = (aa $$ (P9,SUM1)) by A4, A8, A6, XBOOLE_0:def 10;

        end;

          suppose

           A10: FP <> {} ;

          

           A11: ( 0. K) = ( the_unity_wrt aa) by FVSUM_1: 7;

          

           A12: (SUM1 .: FP) c= {( 0. K)}

          proof

            let s be object;

            assume s in (SUM1 .: FP);

            then

            consider x be object such that x in ( dom SUM1) and

             A13: x in FP and

             A14: s = (SUM1 . x) by FUNCT_1:def 6;

            reconsider f = x as Function of X, X by A13, FUNCT_2: 66;

             not f in P by A13, XBOOLE_0:def 5;

            then

             A15: ( Det (B * f)) = ( 0. K) by A0, Th54;

            ex Path be FinSequence of K st ( len Path) = n & (for Fj,j be Nat st j in ( Seg n) & Fj = (f . j) holds (Path . j) = (A * (j,Fj))) & (SUM1 . f) = ((mm $$ Path) * ( Det (B * f))) by A3;

            then (SUM1 . f) = ( 0. K) by A15;

            hence thesis by A14, TARSKI:def 1;

          end;

          ( dom SUM1) = F by FUNCT_2:def 1;

          then (SUM1 .: FP) = {( 0. K)} by A10, A12, ZFMISC_1: 33;

          then

           A16: (aa $$ (FP,SUM1)) = ( 0. K) by A11, FVSUM_1: 8, SETWOP_2: 8;

          

           A17: FP misses P by XBOOLE_1: 79;

          

           A18: (FP \/ P) = (F \/ P) by XBOOLE_1: 39;

          (F \/ P) = F by A6, XBOOLE_1: 12;

          

          hence ( Det AB) = ((aa $$ (P9,SUM1)) + ( 0. K)) by A4, A8, A16, A17, A18, FVSUM_1: 8, SETWOP_2: 4

          .= (aa $$ (P9,SUM1)) by RLVECT_1: 4;

        end;

      end;

      ( dom SUM1) = F by FUNCT_2:def 1;

      then

       A19: ( dom (SUM1 | P)) = P by A6, RELAT_1: 62;

      ( rng (SUM1 | P)) c= KK by RELAT_1:def 19;

      then

      reconsider SP = (SUM1 | P) as Function of P, KK by A19, FUNCT_2: 2;

      take SP;

      

       A20: ( rng ( id P)) = P;

      (SP * ( id P)) = SP by A19, RELAT_1: 52;

      hence ( Det AB) = (aa $$ (( In (P,( Fin P))),SP)) by A9, A2, A20, A7, SETWOP_2: 5;

      let perm be Element of P;

      reconsider Perm = perm as Permutation of X by MATRIX_1:def 12;

      (SUM1 . Perm) = (SP . Perm) by A19, FUNCT_1: 47;

      then

      consider Path be FinSequence of K such that

       A21: ( len Path) = n and

       A22: for Fj,j be Nat st j in ( Seg n) & Fj = (Perm . j) holds (Path . j) = (A * (j,Fj)) and

       A23: (SP . Perm) = ((mm $$ Path) * ( Det (B * Perm))) by A3;

      set PM = ( Path_matrix (perm,A));

      

       A24: ( len PM) = n by MATRIX_3:def 7;

      now

        

         A25: X = ( dom Perm) by FUNCT_2: 52;

        let i be Nat such that

         A26: 1 <= i and

         A27: i <= ( len Path);

        

         A28: i in X by A21, A26, A27;

        i in X by A21, A26, A27;

        then

         A29: (Perm . i) in ( rng Perm) by A25, FUNCT_1:def 3;

        ( rng Perm) c= X by RELAT_1:def 19;

        then (Perm . i) in X by A29;

        then

        reconsider Pi = (Perm . i) as Element of NAT ;

        ( dom PM) = X by A24, FINSEQ_1:def 3;

        then (PM . i) = (A * (i,Pi)) by A28, MATRIX_3:def 7;

        hence (Path . i) = (PM . i) by A22, A28;

      end;

      then Path = PM by A21, A24;

      hence thesis by A23, A0, Th46;

    end;

    theorem :: MATRIX11:62

    K is non degenerated well-unital domRing-like implies for A,B be Matrix of n, K st 0 < n holds ( Det (A * B)) = (( Det A) * ( Det B))

    proof

      assume

       A0: K is non degenerated well-unital domRing-like;

      let A,B be Matrix of n, K such that

       A1: 0 < n;

      set P = ( Permutations n);

      set KK = the carrier of K;

      set mm = the multF of K;

      set aa = the addF of K;

      set AB = (A * B);

      consider SUM1 be Function of P, KK such that

       A2: ( Det AB) = (aa $$ (( In (P,( Fin P))),SUM1)) and

       A3: for perm be Element of ( Permutations n) holds (SUM1 . perm) = ((mm $$ ( Path_matrix (perm,A))) * ( - (( Det B),perm))) by A0, A1, Th61;

      set Path = ( Path_product A);

      set F = ( In (P,( Fin P)));

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

      then

       A4: F = P by SUBSET_1:def 8;

      then

      consider Ga be Function of ( Fin P), KK such that

       A5: ( Det A) = (Ga . F) and

       A6: for e be Element of KK st e is_a_unity_wrt aa holds (Ga . {} ) = e and

       A7: for x be Element of P holds (Ga . {x}) = (Path . x) and

       A8: for B9 be Element of ( Fin P) st B9 c= F & B9 <> {} holds for x be Element of P st x in (F \ B9) holds (Ga . (B9 \/ {x})) = (aa . ((Ga . B9),(Path . x))) by SETWISEO:def 3;

      

       A9: (Ga . {} ) = ( 0. K) by A6, FVSUM_1: 6;

      consider Gs be Function of ( Fin P), KK such that

       A10: ( Det AB) = (Gs . F) and

       A11: for e be Element of KK st e is_a_unity_wrt aa holds (Gs . {} ) = e and

       A12: for x be Element of P holds (Gs . {x}) = (SUM1 . x) and

       A13: for B9 be Element of ( Fin P) st B9 c= F & B9 <> {} holds for x be Element of P st x in (F \ B9) holds (Gs . (B9 \/ {x})) = (aa . ((Gs . B9),(SUM1 . x))) by A2, A4, SETWISEO:def 3;

      defpred S[ set] means for B9 be Element of ( Fin P) st B9 = $1 holds (Gs . B9) = ((Ga . B9) * ( Det B));

      

       A14: for B9 be Element of ( Fin P), b be Element of P holds S[B9] & not b in B9 implies S[(B9 \/ {b})]

      proof

        let B9 be Element of ( Fin P), b be Element of P;

        assume that

         A15: S[B9] and

         A16: not b in B9;

        set mA = (mm $$ ( Path_matrix (b,A)));

        let Bb be Element of ( Fin P) such that

         A17: Bb = (B9 \/ {b});

         A18:

        now

          per cases ;

            suppose

             A19: b is even;

            then

             A20: ( - (mA,b)) = mA by MATRIX_1:def 16;

            ( - (( Det B),b)) = ( Det B) by A19, MATRIX_1:def 16;

            

            hence (SUM1 . b) = (( - (mA,b)) * ( Det B)) by A3, A20

            .= ((Path . b) * ( Det B)) by MATRIX_3:def 8;

          end;

            suppose

             A21: b is odd;

            then

             A22: ( - (mA,b)) = ( - mA) by MATRIX_1:def 16;

            ( - (( Det B),b)) = ( - ( Det B)) by A21, MATRIX_1:def 16;

            

            then ( - (( - (mA,b)) * ( Det B))) = (( - mA) * ( - (( Det B),b))) by A22, VECTSP_1: 9

            .= ( - (mA * ( - (( Det B),b)))) by VECTSP_1: 9;

            then ((mA * ( - (( Det B),b))) - (( - (mA,b)) * ( Det B))) = ( 0. K) by VECTSP_1: 16;

            then

             A23: (( - (mA,b)) * ( Det B)) = (mA * ( - (( Det B),b))) by VECTSP_1: 19;

            ( - (mA,b)) = (Path . b) by MATRIX_3:def 8;

            hence (SUM1 . b) = ((Path . b) * ( Det B)) by A3, A23;

          end;

        end;

        per cases ;

          suppose

           A24: B9 = {} ;

          then (Ga . Bb) = (Path . b) by A7, A17;

          hence thesis by A12, A17, A18, A24;

        end;

          suppose

           A25: B9 <> {} ;

          

           A26: B9 c= P by FINSUB_1:def 5;

          

           A27: b in (F \ B9) by A4, A16, XBOOLE_0:def 5;

          then (Gs . Bb) = (aa . ((Gs . B9),(SUM1 . b))) by A4, A13, A17, A25, A26;

          then

           A28: (Gs . Bb) = (((Ga . B9) * ( Det B)) + ((Path . b) * ( Det B))) by A15, A18;

          (Ga . Bb) = ((Ga . B9) + (Path . b)) by A4, A8, A17, A25, A27, A26;

          hence thesis by A28, VECTSP_1:def 7;

        end;

      end;

      (Gs . {} ) = ( 0. K) by A11, FVSUM_1: 6;

      then

       A29: S[( {}. P)] by A9;

      for B be Element of ( Fin P) holds S[B] from SETWISEO:sch 2( A29, A14);

      hence thesis by A10, A5;

    end;