matrix_9.miz



    begin

    reserve x for set,

i,j,k,n for Nat,

K for Field;

    theorem :: MATRIX_9:1

    

     Th1: for a,A be set st a in A holds {a} in ( Fin A)

    proof

      let a,A be set;

      assume a in A;

      then {a} c= A by ZFMISC_1: 31;

      hence thesis by FINSUB_1:def 5;

    end;

    registration

      let n be Nat;

      cluster non empty for Element of ( Fin ( Permutations n));

      existence

      proof

        ( idseq n) in ( Permutations n) by MATRIX_1:def 12;

        then {( idseq n)} in ( Fin ( Permutations n)) by Th1;

        hence thesis;

      end;

    end

    scheme :: MATRIX_9:sch1

    NonEmptyFiniteX { n() -> Element of NAT , A() -> non empty Element of ( Fin ( Permutations n())) , P[ set] } :

P[A()]

      provided

       A1: for x be Element of ( Permutations n()) st x in A() holds P[ {x}]

       and

       A2: for x be Element of ( Permutations n()), B be non empty Element of ( Fin ( Permutations n())) st x in A() & B c= A() & not x in B & P[B] holds P[(B \/ {x})];

      defpred Q[ set] means $1 is empty or P[$1];

      

       A3: for x,B be set st x in A() & B c= A() & Q[B] holds Q[(B \/ {x})]

      proof

        let x,B be set;

        assume that

         A4: x in A() and

         A5: B c= A() and

         A6: Q[B];

        

         A7: A() c= ( Permutations n()) by FINSUB_1:def 5;

        then

        reconsider x as Element of ( Permutations n()) by A4;

        

         A8: B c= ( Permutations n()) by A5, A7, XBOOLE_1: 1;

        per cases ;

          suppose

           A9: x in B;

          then

          reconsider B as non empty Element of ( Fin ( Permutations n())) by A8, FINSUB_1:def 5;

           {x} c= B by A9, ZFMISC_1: 31;

          hence thesis by A6, XBOOLE_1: 12;

        end;

          suppose

           A10: B is non empty & not x in B;

          then

          reconsider B as non empty Element of ( Fin ( Permutations n())) by A8, FINSUB_1:def 5;

          P[(B \/ {x})] by A2, A4, A5, A6, A10;

          hence thesis;

        end;

          suppose B is empty;

          then P[(B \/ {x})] by A1, A4;

          hence thesis;

        end;

      end;

      

       A11: Q[ {} ];

      

       A12: A() is finite;

       Q[A()] from FINSET_1:sch 2( A12, A11, A3);

      hence thesis;

    end;

    

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

    

     Lm2: <*2, 1*> in ( Permutations 2) by MATRIX_7: 3, TARSKI:def 2;

    registration

      let n;

      cluster one-to-one FinSequence-like for Function of ( Seg n), ( Seg n);

      existence

      proof

        take f = ( id ( Seg n));

        ( dom f) = ( Seg n) by RELAT_1: 45;

        hence thesis by FINSEQ_1:def 2;

      end;

    end

    registration

      let n;

      cluster ( id ( Seg n)) -> FinSequence-like;

      coherence

      proof

        ( dom ( id ( Seg n))) = ( Seg n) by RELAT_1: 45;

        hence thesis by FINSEQ_1:def 2;

      end;

    end

    theorem :: MATRIX_9:2

    

     Th2: (( Rev ( idseq 2)) . 1) = 2 & (( Rev ( idseq 2)) . 2) = 1

    proof

      reconsider f = ( idseq 2) as one-to-one FinSequence-like Function of ( Seg 2), ( Seg 2);

      (f . 1) = (( Rev f) . ( len f)) by FINSEQ_5: 62;

      then

       A1: (( idseq 2) . 1) = (( Rev ( idseq 2)) . 2) by CARD_1:def 7;

      (f . ( len f)) = (( Rev f) . 1) by FINSEQ_5: 62;

      then

       A2: (f . 2) = (( Rev f) . 1) by CARD_1:def 7;

      

       A3: ( dom ( Rev f)) = ( dom f) by FINSEQ_5: 57;

      then

       A4: ( dom ( Rev f)) = ( Seg 2) by RELAT_1: 45;

      then 1 in ( dom f) & 2 in ( dom f) by A3;

      hence thesis by A1, A2, A3, A4, FUNCT_1: 18;

    end;

    theorem :: MATRIX_9:3

    

     Th3: for f be one-to-one Function st ( dom f) = ( Seg 2) & ( rng f) = ( Seg 2) holds f = ( id ( Seg 2)) or f = ( Rev ( id ( Seg 2)))

    proof

      let f be one-to-one Function;

      

       A1: ( dom ( idseq 2)) = ( Seg 2) by RELAT_1: 45;

      assume that

       A2: ( dom f) = ( Seg 2) and

       A3: ( rng f) = ( Seg 2);

      

       A4: 1 in ( dom f) by A2;

      then (f . 1) in ( rng f) by FUNCT_1: 3;

      then

       A5: (f . 1) = 1 or (f . 1) = 2 by A3, FINSEQ_1: 2, TARSKI:def 2;

      

       A6: 2 in ( dom f) by A2;

      then (f . 2) in ( rng f) by FUNCT_1: 3;

      then

       A7: (f . 2) = 2 or (f . 2) = 1 by A3, FINSEQ_1: 2, TARSKI:def 2;

      per cases by A4, A5, A6, A7, FUNCT_1:def 4;

        suppose

         A8: (f . 1) = 1 & (f . 2) = 2;

        for x be object st x in ( Seg 2) holds (f . x) = x

        proof

          let x be object;

          assume x in ( Seg 2);

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

          hence thesis by A8;

        end;

        hence thesis by A2, FUNCT_1: 17;

      end;

        suppose

         A9: (f . 1) = 2 & (f . 2) = 1;

        

         A10: for x be object st x in ( Seg 2) holds (f . x) = (( Rev ( id ( Seg 2))) . x)

        proof

          let x be object;

          assume x in ( Seg 2);

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

          hence thesis by A9, Th2;

        end;

        ( dom f) = ( dom ( Rev ( id ( Seg 2)))) by A1, A2, FINSEQ_5: 57;

        hence thesis by A2, A10, FUNCT_1: 2;

      end;

    end;

    begin

    theorem :: MATRIX_9:4

    

     Th4: ( Rev ( idseq n)) in ( Permutations n)

    proof

      reconsider f = ( idseq n) as one-to-one FinSequence-like Function of ( Seg n), ( Seg n);

      ( dom f) = ( dom ( Rev f)) by FINSEQ_5: 57;

      then

       A1: ( dom ( Rev f)) = ( Seg n) by RELAT_1: 45;

      

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

      then ( rng ( Rev f)) c= ( Seg n) by FINSEQ_5: 57;

      then

      reconsider g = ( Rev f) as FinSequence-like Function of ( Seg n), ( Seg n) by A1, FUNCT_2: 2;

      ( rng f) = ( rng ( Rev f)) by FINSEQ_5: 57;

      then g is onto by A2, FUNCT_2:def 3;

      hence thesis by MATRIX_1:def 12;

    end;

    theorem :: MATRIX_9:5

    

     Th5: for f be FinSequence st n <> 0 & f in ( Permutations n) holds ( Rev f) in ( Permutations n)

    proof

      let f be FinSequence;

      assume that

       A1: n <> 0 and

       A2: f in ( Permutations n);

      

       A3: f is Permutation of ( Seg n) by A2, MATRIX_1:def 12;

      ( dom f) = ( dom ( Rev f)) by FINSEQ_5: 57;

      then

       A4: ( dom ( Rev f)) = ( Seg n) by A1, A3, FUNCT_2:def 1;

      

       A5: ( rng f) = ( rng ( Rev f)) by FINSEQ_5: 57;

      then ( rng ( Rev f)) = ( Seg n) by A3, FUNCT_2:def 3;

      then

      reconsider g = ( Rev f) as FinSequence-like Function of ( Seg n), ( Seg n) by A4, FUNCT_2: 2;

      ( rng f) = ( Seg n) by A3, FUNCT_2:def 3;

      then g is onto by A5, FUNCT_2:def 3;

      hence thesis by A3, MATRIX_1:def 12;

    end;

    theorem :: MATRIX_9:6

    

     Th6: ( Permutations 2) = {( idseq 2), ( Rev ( idseq 2))}

    proof

      now

        let p be object;

        assume p in ( Permutations 2);

        then

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

        

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

        

         A2: ( dom q) = ( Seg 2) by FUNCT_2: 52;

        then

        reconsider q as FinSequence by FINSEQ_1:def 2;

        q = ( idseq 2) or q = ( Rev ( idseq 2)) by A1, A2, Th3;

        hence p in {( idseq 2), ( Rev ( idseq 2))} by TARSKI:def 2;

      end;

      then

       A3: ( Permutations 2) c= {( idseq 2), ( Rev ( idseq 2))} by TARSKI:def 3;

      now

        let x be object;

        assume x in {( idseq 2), ( Rev ( idseq 2))};

        then x = ( idseq 2) or x = ( Rev ( idseq 2)) by TARSKI:def 2;

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

      end;

      then {( idseq 2), ( Rev ( idseq 2))} c= ( Permutations 2) by TARSKI:def 3;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    begin

    definition

      let n, K;

      let M be Matrix of n, K;

      :: MATRIX_9:def1

      func PPath_product M -> Function of ( Permutations n), the carrier of K means

      : Def1: for p be Element of ( Permutations n) holds (it . p) = (the multF of K $$ ( Path_matrix (p,M)));

      existence

      proof

        deffunc V( Element of ( Permutations n)) = (the multF of K $$ ( Path_matrix ($1,M)));

        consider f be Function of ( Permutations n), the carrier of K such that

         A1: for p be Element of ( Permutations n) holds (f . p) = V(p) from FUNCT_2:sch 4;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be Function of ( Permutations n), the carrier of K;

        assume that

         A2: for p be Element of ( Permutations n) holds (f1 . p) = (the multF of K $$ ( Path_matrix (p,M))) and

         A3: for p be Element of ( Permutations n) holds (f2 . p) = (the multF of K $$ ( Path_matrix (p,M)));

        now

          let p be Element of ( Permutations n);

          (f1 . p) = (the multF of K $$ ( Path_matrix (p,M))) by A2;

          hence (f1 . p) = (f2 . p) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let n, K;

      let M be Matrix of n, K;

      :: MATRIX_9:def2

      func Per M -> Element of K equals (the addF of K $$ (( In (( Permutations n),( Fin ( Permutations n)))),( PPath_product M)));

      coherence ;

    end

    reserve a,b,c,d for Element of K;

    theorem :: MATRIX_9:7

    ( Per <* <*a*>*>) = a

    proof

      set M = <* <*a*>*>;

      

       A1: (( PPath_product M) . ( idseq 1)) = a

      proof

        reconsider p = ( idseq 1) as Element of ( Permutations 1) by MATRIX_1:def 12;

        

         A2: ( len ( Path_matrix (p,M))) = 1 by MATRIX_3:def 7;

        then

         A3: ( dom ( Path_matrix (p,M))) = ( Seg 1) by FINSEQ_1:def 3;

        then

         A4: 1 in ( dom ( Path_matrix (p,M)));

        then 1 = (p . 1) by A3, FUNCT_1: 18;

        then (( Path_matrix (p,M)) . 1) = (M * (1,1)) by A4, MATRIX_3:def 7;

        then (( Path_matrix (p,M)) . 1) = a by MATRIX_0: 49;

        then

         A5: ( Path_matrix (p,M)) = <*a*> by A2, FINSEQ_1: 40;

        (( PPath_product M) . p) = (the multF of K $$ ( Path_matrix (p,M))) & <*a*> = (1 |-> a) by Def1, FINSEQ_2: 59;

        hence thesis by A5, FINSOP_1: 16;

      end;

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

      then ( In (( Permutations 1),( Fin ( Permutations 1)))) = ( Permutations 1) by SUBSET_1:def 8;

      then ( In (( Permutations 1),( Fin ( Permutations 1)))) = {( idseq 1)} & ( idseq 1) in ( Permutations 1) by MATRIX_1: 10, TARSKI:def 1;

      hence thesis by A1, SETWISEO: 17;

    end;

    theorem :: MATRIX_9:8

    for K be Field, n be Element of NAT st n >= 1 holds ( Per ( 0. (K,n,n))) = ( 0. K)

    proof

      let K be Field, n be Element of NAT ;

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

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

      set F = the addF of K;

      set Y = the carrier of K;

      set X = ( Permutations n);

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

      

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

      proof

        let e be Element of Y;

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

        then

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

        assume e is_a_unity_wrt F;

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

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

      end;

      assume

       A3: n >= 1;

      

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

      proof

        let x be object;

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

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

        proof

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

          let p be Element of ( Permutations n);

          

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

          proof

            let k be Nat;

            

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

            assume P[k];

            

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

            .= ( 0. K);

            hence thesis;

          end;

          

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

          proof

            let i, j;

            assume that

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

             A9: j = (p . i);

            

             A10: i in ( Seg n) by A8, FUNCOP_1: 13;

            then j in ( Seg n) by A9, MATRIX_7: 14;

            then

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

            i in ( dom ( 0. (K,n,n))) by A10, MATRIX_7: 13;

            then [i, j] in [:( dom ( 0. (K,n,n))), ( Seg ( width ( 0. (K,n,n)))):] by A11, ZFMISC_1:def 2;

            then

             A12: [i, j] in ( Indices ( 0. (K,n,n))) by MATRIX_0:def 4;

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

            hence thesis by A12, MATRIX_3: 1;

          end;

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

          then

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

          

           A14: ((n -' 1) + 1) = n by A3, XREAL_1: 235;

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

          then

           A15: P[ 0 ] by FINSOP_1: 11;

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

          then (the multF of K $$ ( Path_matrix (p,( 0. (K,n,n))))) = ( 0. K) by A13, A14;

          hence thesis by FUNCOP_1: 7;

        end;

        hence thesis by Def1;

      end;

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

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

      then

       A16: ( PPath_product ( 0. (K,n,n))) = (( Permutations n) --> ( 0. K)) by A4, FUNCT_1: 2;

      

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

      proof

        let x be Element of X;

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

        hence thesis by A16, FUNCOP_1: 7;

      end;

      

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

      proof

        let B9 be Element of ( Fin X);

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

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

        proof

          let x be Element of X;

          assume x in (B \ B9);

          

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

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

          hence thesis by A19, BINOP_1: 3;

        end;

      end;

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

      then ( In (( Permutations n),( Fin ( Permutations n)))) = ( Permutations n) by SUBSET_1:def 8;

      then ( In (( Permutations n),( Fin ( Permutations n)))) <> {} & (G0 . B) = ( 0. K) by FUNCOP_1: 7;

      hence thesis by A1, A17, A18, SETWISEO:def 3;

    end;

    theorem :: MATRIX_9:9

    

     Th9: for p be Element of ( Permutations 2) st p = ( idseq 2) holds ( Path_matrix (p,((a,b) ][ (c,d)))) = <*a, d*>

    proof

      let p be Element of ( Permutations 2) such that

       A1: p = ( idseq 2);

      

       A2: ( len ( Path_matrix (p,((a,b) ][ (c,d))))) = 2 by MATRIX_3:def 7;

      then

       A3: ( dom ( Path_matrix (p,((a,b) ][ (c,d))))) = ( Seg 2) by FINSEQ_1:def 3;

      then

       A4: 2 in ( dom ( Path_matrix (p,((a,b) ][ (c,d)))));

      then 2 = (p . 2) by A1, A3, FUNCT_1: 18;

      

      then

       A5: (( Path_matrix (p,((a,b) ][ (c,d)))) . 2) = (((a,b) ][ (c,d)) * (2,2)) by A4, MATRIX_3:def 7

      .= d by MATRIX_0: 50;

      

       A6: 1 in ( dom ( Path_matrix (p,((a,b) ][ (c,d))))) by A3;

      then 1 = (p . 1) by A1, A3, FUNCT_1: 18;

      

      then (( Path_matrix (p,((a,b) ][ (c,d)))) . 1) = (((a,b) ][ (c,d)) * (1,1)) by A6, MATRIX_3:def 7

      .= a by MATRIX_0: 50;

      hence thesis by A2, A5, FINSEQ_1: 44;

    end;

    theorem :: MATRIX_9:10

    

     Th10: for p be Element of ( Permutations 2) st p = ( Rev ( idseq 2)) holds ( Path_matrix (p,((a,b) ][ (c,d)))) = <*b, c*>

    proof

      let p be Element of ( Permutations 2) such that

       A1: p = ( Rev ( idseq 2));

      

       A2: ( len ( Path_matrix (p,((a,b) ][ (c,d))))) = 2 by MATRIX_3:def 7;

      then

       A3: ( dom ( Path_matrix (p,((a,b) ][ (c,d))))) = ( Seg 2) by FINSEQ_1:def 3;

      then 1 in ( dom ( Path_matrix (p,((a,b) ][ (c,d)))));

      

      then

       A4: (( Path_matrix (p,((a,b) ][ (c,d)))) . 1) = (((a,b) ][ (c,d)) * (1,2)) by A1, Th2, MATRIX_3:def 7

      .= b by MATRIX_0: 50;

      2 in ( dom ( Path_matrix (p,((a,b) ][ (c,d))))) by A3;

      

      then (( Path_matrix (p,((a,b) ][ (c,d)))) . 2) = (((a,b) ][ (c,d)) * (2,1)) by A1, Th2, MATRIX_3:def 7

      .= c by MATRIX_0: 50;

      hence thesis by A2, A4, FINSEQ_1: 44;

    end;

    theorem :: MATRIX_9:11

    

     Th11: (the multF of K $$ <*a, b*>) = (a * b)

    proof

      (the multF of K $$ <*a, b*>) = ( Product <*a, b*>) by GROUP_4:def 2

      .= (a * b) by GROUP_4: 10;

      hence thesis;

    end;

    begin

    registration

      cluster odd for Permutation of ( Seg 2);

      existence

      proof

        reconsider g = <*2, 1*> as Permutation of ( Seg 2) by Lm2, MATRIX_1:def 12;

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

        then g is odd by MATRIX_1:def 15;

        hence thesis;

      end;

    end

    registration

      let n be Nat;

      cluster even for Permutation of ( Seg n);

      existence

      proof

        reconsider f = ( id ( Seg n)) as Permutation of ( Seg n);

        f is even by MATRIX_1: 16;

        hence thesis;

      end;

    end

    theorem :: MATRIX_9:12

    

     Th12: <*2, 1*> is odd Permutation of ( Seg 2)

    proof

      reconsider g = <*2, 1*> as Permutation of ( Seg 2) by Lm2, MATRIX_1:def 12;

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

      hence thesis by MATRIX_1:def 15;

    end;

    theorem :: MATRIX_9:13

    ( Det ((a,b) ][ (c,d))) = ((a * d) - (b * c))

    proof

      reconsider rid2 = ( Rev ( idseq 2)) as Element of ( Permutations 2) by Th4;

      set M = ((a,b) ][ (c,d));

      reconsider id2 = ( idseq 2) as Permutation of ( Seg 2);

      reconsider Id2 = ( idseq 2) as Element of ( Permutations 2) by MATRIX_1:def 12;

      set F = the addF of K;

      set f = ( Path_product M);

      

       A1: rid2 = <*2, 1*> & ( len ( Permutations 2)) = 2 by FINSEQ_2: 52, FINSEQ_5: 61, MATRIX_1: 9;

      

       A2: (f . rid2) = ( - ((the multF of K $$ ( Path_matrix (rid2,M))),rid2)) by MATRIX_3:def 8

      .= ( - (the multF of K $$ ( Path_matrix (rid2,M)))) by A1, Th12, MATRIX_1:def 16

      .= ( - (the multF of K $$ <*b, c*>)) by Th10

      .= ( - (b * c)) by Th11;

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

      then

       A3: Id2 is even by MATRIX_1: 16;

      1 in ( Seg 2);

      then

       A4: id2 <> rid2 by Th2, FUNCT_1: 18;

      

       A5: (f . id2) = ( - ((the multF of K $$ ( Path_matrix (Id2,M))),Id2)) by MATRIX_3:def 8

      .= (the multF of K $$ ( Path_matrix (Id2,M))) by A3, MATRIX_1:def 16

      .= (the multF of K $$ <*a, d*>) by Th9

      .= (a * d) by Th11;

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

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

      

      then ( Det M) = (F $$ ( {.Id2, rid2.},f)) by Th6, MATRIX_3:def 9

      .= ((a * d) - (b * c)) by A5, A4, A2, SETWOP_2: 1;

      hence thesis;

    end;

    theorem :: MATRIX_9:14

    ( Per ((a,b) ][ (c,d))) = ((a * d) + (b * c))

    proof

      reconsider rid2 = ( Rev ( idseq 2)) as Element of ( Permutations 2) by Th4;

      set M = ((a,b) ][ (c,d));

      reconsider Id2 = ( idseq 2) as Element of ( Permutations 2) by MATRIX_1:def 12;

      reconsider id2 = Id2 as Permutation of ( Seg 2);

      set f = ( PPath_product M);

      

       A0: 1 in ( Seg 2);

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

      then

       A1: ( In (( Permutations 2),( Fin ( Permutations 2)))) = ( Permutations 2) & id2 <> rid2 by A0, Th2, FUNCT_1: 18, SUBSET_1:def 8;

      

       A2: (f . rid2) = (the multF of K $$ ( Path_matrix (rid2,M))) by Def1

      .= (the multF of K $$ <*b, c*>) by Th10

      .= (b * c) by Th11;

      (f . id2) = (the multF of K $$ ( Path_matrix (Id2,M))) by Def1

      .= (the multF of K $$ <*a, d*>) by Th9

      .= (a * d) by Th11;

      hence thesis by A2, A1, Th6, SETWOP_2: 1;

    end;

    theorem :: MATRIX_9:15

    

     Th15: ( Rev ( idseq 3)) = <*3, 2, 1*>

    proof

      reconsider h = <*2, 3*> as FinSequence of NAT ;

      ( <*1*> ^ h) = <*1, 2, 3*> & ( Rev h) = <*3, 2*> by FINSEQ_1: 43, FINSEQ_5: 61;

      hence thesis by FINSEQ_2: 53, FINSEQ_6: 24;

    end;

    reserve D for non empty set;

    theorem :: MATRIX_9:16

    for x,y,z be Element of D holds for f be FinSequence of D st f = <*x, y, z*> holds ( Rev f) = <*z, y, x*>

    proof

      let x,y,z be Element of D;

      let f be FinSequence of D;

      reconsider h = <*y, z*> as FinSequence of D;

      assume f = <*x, y, z*>;

      then

       A1: f = ( <*x*> ^ h) by FINSEQ_1: 43;

      ( Rev h) = <*z, y*> by FINSEQ_5: 61;

      hence thesis by A1, FINSEQ_6: 24;

    end;

    theorem :: MATRIX_9:17

    

     Th17: for f,g be FinSequence st (f ^ g) in ( Permutations n) holds (f ^ ( Rev g)) in ( Permutations n)

    proof

      let f,g be FinSequence;

      

       A1: ( rng g) = ( rng ( Rev g)) by FINSEQ_5: 57;

      set h = (f ^ ( Rev g));

      assume (f ^ g) in ( Permutations n);

      then

       A2: (f ^ g) is Permutation of ( Seg n) by MATRIX_1:def 12;

      then

       A3: g is one-to-one by FINSEQ_3: 91;

      ( dom (f ^ g)) = ( Seg n) by A2, FUNCT_2: 52;

      then

       A4: ( Seg n) = ( Seg (( len f) + ( len g))) by FINSEQ_1:def 7;

      ( len g) = ( len ( Rev g)) by FINSEQ_5:def 3;

      then

       A5: ( dom h) = ( Seg n) by A4, FINSEQ_1:def 7;

      

       A6: ( rng (f ^ g)) = (( rng f) \/ ( rng g)) by FINSEQ_1: 31

      .= ( rng (f ^ ( Rev g))) by A1, FINSEQ_1: 31;

      

       A7: ( rng (f ^ g)) = ( Seg n) by A2, FUNCT_2:def 3;

      then

      reconsider h as FinSequence-like Function of ( Seg n), ( Seg n) by A6, A5, FUNCT_2: 2;

      

       A8: h is onto by A7, A6, FUNCT_2:def 3;

      ( rng f) misses ( rng g) & f is one-to-one by A2, FINSEQ_3: 91;

      then h is one-to-one by A1, A3, FINSEQ_3: 91;

      hence thesis by A8, MATRIX_1:def 12;

    end;

    theorem :: MATRIX_9:18

    

     Th18: for f,g be FinSequence st (f ^ g) in ( Permutations n) holds (g ^ f) in ( Permutations n)

    proof

      let f,g be FinSequence;

      

       A1: ( Seg ( len (f ^ g))) = ( dom (f ^ g)) by FINSEQ_1:def 3;

      ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22

      .= ( len (g ^ f)) by FINSEQ_1: 22;

      then

       A2: ( dom (f ^ g)) = ( dom (g ^ f)) by A1, FINSEQ_1:def 3;

      

       A3: ( rng (f ^ g)) = (( rng f) \/ ( rng g)) by FINSEQ_1: 31

      .= ( rng (g ^ f)) by FINSEQ_1: 31;

      assume (f ^ g) in ( Permutations n);

      then

       A4: (f ^ g) is Permutation of ( Seg n) by MATRIX_1:def 12;

      then

       A5: ( rng (f ^ g)) = ( Seg n) by FUNCT_2:def 3;

      

       A6: g is one-to-one by A4, FINSEQ_3: 91;

      ( dom (f ^ g)) = ( Seg n) by A4, FUNCT_2: 52;

      then

      reconsider h = (g ^ f) as FinSequence-like Function of ( Seg n), ( Seg n) by A5, A2, A3, FUNCT_2: 2;

      ( rng f) misses ( rng g) & f is one-to-one by A4, FINSEQ_3: 91;

      then

       A7: h is one-to-one by A6, FINSEQ_3: 91;

      h is onto by A5, A3, FUNCT_2:def 3;

      hence thesis by A7, MATRIX_1:def 12;

    end;

    theorem :: MATRIX_9:19

    

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

    proof

      now

        let x be object;

        

         A1: ( idseq 3) in ( Permutations 3) by MATRIX_1:def 12;

        

         A2: <*3, 1, 2*> in ( Permutations 3)

        proof

          reconsider h = <*1, 2*> as FinSequence of NAT ;

          ( <*3*> ^ h) = <*3, 1, 2*> by FINSEQ_1: 43;

          hence thesis by A1, Th18, FINSEQ_2: 53;

        end;

        

         A3: <*2, 3, 1*> in ( Permutations 3)

        proof

          reconsider h = <*2, 3*> as FinSequence of NAT ;

          reconsider f = <*1, 2, 3*> as one-to-one FinSequence-like Function of ( Seg 3), ( Seg 3) by FINSEQ_2: 53;

          f = ( <*1*> ^ h) by FINSEQ_1: 43;

          hence thesis by A1, Th18, FINSEQ_2: 53;

        end;

        

         A4: <*1, 3, 2*> in ( Permutations 3)

        proof

          reconsider h = <*2, 3*> as FinSequence of NAT ;

          reconsider f = <*1, 2, 3*> as one-to-one FinSequence-like Function of ( Seg 3), ( Seg 3) by FINSEQ_2: 53;

          ( Rev h) = <*3, 2*> by FINSEQ_5: 61;

          then f = ( <*1*> ^ h) & ( <*1*> ^ ( Rev h)) = <*1, 3, 2*> by FINSEQ_1: 43;

          hence thesis by A1, Th17, FINSEQ_2: 53;

        end;

        

         A5: <*2, 1, 3*> in ( Permutations 3)

        proof

          reconsider h = <*1, 2*> as FinSequence of NAT ;

          ( <*3*> ^ h) in ( Permutations 3) by A1, Th18, FINSEQ_2: 53;

          then ( Rev h) = <*2, 1*> & ( <*3*> ^ ( Rev h)) in ( Permutations 3) by Th17, FINSEQ_5: 61;

          hence thesis by Th18;

        end;

        assume x in { <*1, 2, 3*>, <*3, 2, 1*>, <*1, 3, 2*>, <*2, 3, 1*>, <*2, 1, 3*>, <*3, 1, 2*>};

        then x in ( { <*1, 2, 3*>, <*3, 2, 1*>} \/ { <*1, 3, 2*>, <*2, 3, 1*>, <*2, 1, 3*>, <*3, 1, 2*>}) by ENUMSET1: 12;

        then x in { <*1, 2, 3*>, <*3, 2, 1*>} or x in { <*1, 3, 2*>, <*2, 3, 1*>, <*2, 1, 3*>, <*3, 1, 2*>} by XBOOLE_0:def 3;

        then x in { <*1, 2, 3*>, <*3, 2, 1*>} or x in ( { <*1, 3, 2*>, <*2, 3, 1*>} \/ { <*2, 1, 3*>, <*3, 1, 2*>}) by ENUMSET1: 5;

        then

         A6: x in { <*1, 2, 3*>, <*3, 2, 1*>} or x in { <*1, 3, 2*>, <*2, 3, 1*>} or x in { <*2, 1, 3*>, <*3, 1, 2*>} by XBOOLE_0:def 3;

        ( Rev ( idseq 3)) in ( Permutations 3) by Th4;

        hence x in ( Permutations 3) by A6, A1, A4, A3, A5, A2, Th15, FINSEQ_2: 53, TARSKI:def 2;

      end;

      then

       A7: { <*1, 2, 3*>, <*3, 2, 1*>, <*1, 3, 2*>, <*2, 3, 1*>, <*2, 1, 3*>, <*3, 1, 2*>} c= ( Permutations 3) by TARSKI:def 3;

      now

        let p be object;

        assume p in ( Permutations 3);

        then

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

        

         A8: ( rng q) = ( Seg 3) by FUNCT_2:def 3;

        

         A9: 3 in ( Seg 3);

        then (q . 3) in ( Seg 3) by A8, FUNCT_2: 4;

        then

         A10: (q . 3) = 1 or (q . 3) = 2 or (q . 3) = 3 by ENUMSET1:def 1, FINSEQ_3: 1;

        

         A11: 2 in ( Seg 3);

        then (q . 2) in ( Seg 3) by A8, FUNCT_2: 4;

        then

         A12: (q . 2) = 1 or (q . 2) = 2 or (q . 2) = 3 by ENUMSET1:def 1, FINSEQ_3: 1;

        

         A13: ( dom q) = ( Seg 3) by FUNCT_2: 52;

        

         A14: (q . 1) = 1 & (q . 2) = 2 & (q . 3) = 3 or (q . 1) = 3 & (q . 2) = 2 & (q . 3) = 1 or (q . 1) = 1 & (q . 2) = 3 & (q . 3) = 2 or (q . 1) = 2 & (q . 2) = 3 & (q . 3) = 1 or (q . 1) = 2 & (q . 2) = 1 & (q . 3) = 3 or (q . 1) = 3 & (q . 2) = 1 & (q . 3) = 2 implies q = <*1, 2, 3*> or q = <*3, 2, 1*> or q = <*1, 3, 2*> or q = <*2, 3, 1*> or q = <*2, 1, 3*> or q = <*3, 1, 2*>

        proof

          reconsider q as FinSequence by A13, FINSEQ_1:def 2;

          ( len q) = 3 by A13, FINSEQ_1:def 3;

          hence thesis by FINSEQ_1: 45;

        end;

        

         A15: 1 in ( Seg 3);

        then (q . 1) in ( Seg 3) by A8, FUNCT_2: 4;

        then (q . 1) = 1 or (q . 1) = 2 or (q . 1) = 3 by ENUMSET1:def 1, FINSEQ_3: 1;

        then p = <*1, 2, 3*> or p = <*3, 2, 1*> or q = <*1, 3, 2*> or q = <*2, 3, 1*> or q = <*2, 1, 3*> or q = <*3, 1, 2*> by A13, A15, A11, A9, A12, A10, A14, FUNCT_1:def 4;

        then p in { <*1, 2, 3*>, <*3, 2, 1*>} or q in { <*1, 3, 2*>, <*2, 3, 1*>} or q in { <*2, 1, 3*>, <*3, 1, 2*>} by TARSKI:def 2;

        then p in { <*1, 2, 3*>, <*3, 2, 1*>} or q in ( { <*1, 3, 2*>, <*2, 3, 1*>} \/ { <*2, 1, 3*>, <*3, 1, 2*>}) by XBOOLE_0:def 3;

        then p in { <*1, 2, 3*>, <*3, 2, 1*>} or q in { <*1, 3, 2*>, <*2, 3, 1*>, <*2, 1, 3*>, <*3, 1, 2*>} by ENUMSET1: 5;

        then p in ( { <*1, 2, 3*>, <*3, 2, 1*>} \/ { <*1, 3, 2*>, <*2, 3, 1*>, <*2, 1, 3*>, <*3, 1, 2*>}) by XBOOLE_0:def 3;

        hence p in { <*1, 2, 3*>, <*3, 2, 1*>, <*1, 3, 2*>, <*2, 3, 1*>, <*2, 1, 3*>, <*3, 1, 2*>} by ENUMSET1: 12;

      end;

      then ( Permutations 3) c= { <*1, 2, 3*>, <*3, 2, 1*>, <*1, 3, 2*>, <*2, 3, 1*>, <*2, 1, 3*>, <*3, 1, 2*>} by TARSKI:def 3;

      hence thesis by A7, XBOOLE_0:def 10;

    end;

    theorem :: MATRIX_9:20

    

     Th20: for a,b,c,d,e,f,g,h,i be Element of K holds for M be Matrix of 3, K st M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*> holds for p be Element of ( Permutations 3) st p = <*1, 2, 3*> holds ( Path_matrix (p,M)) = <*a, e, i*>

    proof

      let a,b,c,d,e,f,g,h,i be Element of K;

      let M be Matrix of 3, K;

       [1, 1] in ( Indices M) by MATRIX_0: 31;

      then

      consider r be FinSequence of the carrier of K such that

       A1: r = (M . 1) and

       A2: (M * (1,1)) = (r . 1) by MATRIX_0:def 5;

      assume

       A3: M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*>;

      then (M . 1) = <*a, b, c*> by FINSEQ_1: 45;

      then

       A4: (r . 1) = a by A1, FINSEQ_1: 45;

       [3, 3] in ( Indices M) by MATRIX_0: 31;

      then

      consider z be FinSequence of the carrier of K such that

       A5: z = (M . 3) and

       A6: (M * (3,3)) = (z . 3) by MATRIX_0:def 5;

      (M . 3) = <*g, h, i*> by A3, FINSEQ_1: 45;

      then

       A7: (z . 3) = i by A5, FINSEQ_1: 45;

       [2, 2] in ( Indices M) by MATRIX_0: 31;

      then

      consider y be FinSequence of the carrier of K such that

       A8: y = (M . 2) and

       A9: (M * (2,2)) = (y . 2) by MATRIX_0:def 5;

      (M . 2) = <*d, e, f*> by A3, FINSEQ_1: 45;

      then

       A10: (y . 2) = e by A8, FINSEQ_1: 45;

      let p be Element of ( Permutations 3);

      assume

       A11: p = <*1, 2, 3*>;

      then

       A12: 1 = (p . 1) by FINSEQ_1: 45;

      

       A13: 3 = (p . 3) by A11, FINSEQ_1: 45;

      

       A14: 2 = (p . 2) by A11, FINSEQ_1: 45;

      

       A15: ( len ( Path_matrix (p,M))) = 3 by MATRIX_3:def 7;

      then

       A16: ( dom ( Path_matrix (p,M))) = ( Seg 3) by FINSEQ_1:def 3;

      then 2 in ( dom ( Path_matrix (p,M)));

      then

       A17: (( Path_matrix (p,M)) . 2) = e by A14, A9, A10, MATRIX_3:def 7;

      3 in ( dom ( Path_matrix (p,M))) by A16;

      then

       A18: (( Path_matrix (p,M)) . 3) = i by A13, A6, A7, MATRIX_3:def 7;

      1 in ( dom ( Path_matrix (p,M))) by A16;

      then (( Path_matrix (p,M)) . 1) = a by A12, A2, A4, MATRIX_3:def 7;

      hence thesis by A15, A17, A18, FINSEQ_1: 45;

    end;

    theorem :: MATRIX_9:21

    

     Th21: for a,b,c,d,e,f,g,h,i be Element of K holds for M be Matrix of 3, K st M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*> holds for p be Element of ( Permutations 3) st p = <*3, 2, 1*> holds ( Path_matrix (p,M)) = <*c, e, g*>

    proof

      let a,b,c,d,e,f,g,h,i be Element of K;

      let M be Matrix of 3, K;

       [1, 3] in ( Indices M) by MATRIX_0: 31;

      then

      consider r be FinSequence of the carrier of K such that

       A1: r = (M . 1) and

       A2: (M * (1,3)) = (r . 3) by MATRIX_0:def 5;

      assume

       A3: M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*>;

      then (M . 1) = <*a, b, c*> by FINSEQ_1: 45;

      then

       A4: (r . 3) = c by A1, FINSEQ_1: 45;

       [3, 1] in ( Indices M) by MATRIX_0: 31;

      then

      consider z be FinSequence of the carrier of K such that

       A5: z = (M . 3) and

       A6: (M * (3,1)) = (z . 1) by MATRIX_0:def 5;

      (M . 3) = <*g, h, i*> by A3, FINSEQ_1: 45;

      then

       A7: (z . 1) = g by A5, FINSEQ_1: 45;

       [2, 2] in ( Indices M) by MATRIX_0: 31;

      then

      consider y be FinSequence of the carrier of K such that

       A8: y = (M . 2) and

       A9: (M * (2,2)) = (y . 2) by MATRIX_0:def 5;

      (M . 2) = <*d, e, f*> by A3, FINSEQ_1: 45;

      then

       A10: (y . 2) = e by A8, FINSEQ_1: 45;

      let p be Element of ( Permutations 3);

      assume

       A11: p = <*3, 2, 1*>;

      then

       A12: 3 = (p . 1) by FINSEQ_1: 45;

      

       A13: 1 = (p . 3) by A11, FINSEQ_1: 45;

      

       A14: 2 = (p . 2) by A11, FINSEQ_1: 45;

      

       A15: ( len ( Path_matrix (p,M))) = 3 by MATRIX_3:def 7;

      then

       A16: ( dom ( Path_matrix (p,M))) = ( Seg 3) by FINSEQ_1:def 3;

      then 2 in ( dom ( Path_matrix (p,M)));

      then

       A17: (( Path_matrix (p,M)) . 2) = e by A14, A9, A10, MATRIX_3:def 7;

      3 in ( dom ( Path_matrix (p,M))) by A16;

      then

       A18: (( Path_matrix (p,M)) . 3) = g by A13, A6, A7, MATRIX_3:def 7;

      1 in ( dom ( Path_matrix (p,M))) by A16;

      then (( Path_matrix (p,M)) . 1) = c by A12, A2, A4, MATRIX_3:def 7;

      hence thesis by A15, A17, A18, FINSEQ_1: 45;

    end;

    theorem :: MATRIX_9:22

    

     Th22: for a,b,c,d,e,f,g,h,i be Element of K holds for M be Matrix of 3, K st M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*> holds for p be Element of ( Permutations 3) st p = <*1, 3, 2*> holds ( Path_matrix (p,M)) = <*a, f, h*>

    proof

      let a,b,c,d,e,f,g,h,i be Element of K;

      let M be Matrix of 3, K;

       [1, 1] in ( Indices M) by MATRIX_0: 31;

      then

      consider r be FinSequence of the carrier of K such that

       A1: r = (M . 1) and

       A2: (M * (1,1)) = (r . 1) by MATRIX_0:def 5;

      assume

       A3: M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*>;

      then (M . 1) = <*a, b, c*> by FINSEQ_1: 45;

      then

       A4: (r . 1) = a by A1, FINSEQ_1: 45;

       [3, 2] in ( Indices M) by MATRIX_0: 31;

      then

      consider z be FinSequence of the carrier of K such that

       A5: z = (M . 3) and

       A6: (M * (3,2)) = (z . 2) by MATRIX_0:def 5;

      (M . 3) = <*g, h, i*> by A3, FINSEQ_1: 45;

      then

       A7: (z . 2) = h by A5, FINSEQ_1: 45;

       [2, 3] in ( Indices M) by MATRIX_0: 31;

      then

      consider y be FinSequence of the carrier of K such that

       A8: y = (M . 2) and

       A9: (M * (2,3)) = (y . 3) by MATRIX_0:def 5;

      (M . 2) = <*d, e, f*> by A3, FINSEQ_1: 45;

      then

       A10: (y . 3) = f by A8, FINSEQ_1: 45;

      let p be Element of ( Permutations 3);

      assume

       A11: p = <*1, 3, 2*>;

      then

       A12: 1 = (p . 1) by FINSEQ_1: 45;

      

       A13: 2 = (p . 3) by A11, FINSEQ_1: 45;

      

       A14: 3 = (p . 2) by A11, FINSEQ_1: 45;

      

       A15: ( len ( Path_matrix (p,M))) = 3 by MATRIX_3:def 7;

      then

       A16: ( dom ( Path_matrix (p,M))) = ( Seg 3) by FINSEQ_1:def 3;

      then 2 in ( dom ( Path_matrix (p,M)));

      then

       A17: (( Path_matrix (p,M)) . 2) = f by A14, A9, A10, MATRIX_3:def 7;

      3 in ( dom ( Path_matrix (p,M))) by A16;

      then

       A18: (( Path_matrix (p,M)) . 3) = h by A13, A6, A7, MATRIX_3:def 7;

      1 in ( dom ( Path_matrix (p,M))) by A16;

      then (( Path_matrix (p,M)) . 1) = a by A12, A2, A4, MATRIX_3:def 7;

      hence thesis by A15, A17, A18, FINSEQ_1: 45;

    end;

    theorem :: MATRIX_9:23

    

     Th23: for a,b,c,d,e,f,g,h,i be Element of K holds for M be Matrix of 3, K st M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*> holds for p be Element of ( Permutations 3) st p = <*2, 3, 1*> holds ( Path_matrix (p,M)) = <*b, f, g*>

    proof

      let a,b,c,d,e,f,g,h,i be Element of K;

      let M be Matrix of 3, K;

       [1, 2] in ( Indices M) by MATRIX_0: 31;

      then

      consider r be FinSequence of the carrier of K such that

       A1: r = (M . 1) and

       A2: (M * (1,2)) = (r . 2) by MATRIX_0:def 5;

      assume

       A3: M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*>;

      then (M . 1) = <*a, b, c*> by FINSEQ_1: 45;

      then

       A4: (r . 2) = b by A1, FINSEQ_1: 45;

       [3, 1] in ( Indices M) by MATRIX_0: 31;

      then

      consider z be FinSequence of the carrier of K such that

       A5: z = (M . 3) and

       A6: (M * (3,1)) = (z . 1) by MATRIX_0:def 5;

      (M . 3) = <*g, h, i*> by A3, FINSEQ_1: 45;

      then

       A7: (z . 1) = g by A5, FINSEQ_1: 45;

       [2, 3] in ( Indices M) by MATRIX_0: 31;

      then

      consider y be FinSequence of the carrier of K such that

       A8: y = (M . 2) and

       A9: (M * (2,3)) = (y . 3) by MATRIX_0:def 5;

      (M . 2) = <*d, e, f*> by A3, FINSEQ_1: 45;

      then

       A10: (y . 3) = f by A8, FINSEQ_1: 45;

      let p be Element of ( Permutations 3);

      assume

       A11: p = <*2, 3, 1*>;

      then

       A12: 2 = (p . 1) by FINSEQ_1: 45;

      

       A13: 1 = (p . 3) by A11, FINSEQ_1: 45;

      

       A14: 3 = (p . 2) by A11, FINSEQ_1: 45;

      

       A15: ( len ( Path_matrix (p,M))) = 3 by MATRIX_3:def 7;

      then

       A16: ( dom ( Path_matrix (p,M))) = ( Seg 3) by FINSEQ_1:def 3;

      then 2 in ( dom ( Path_matrix (p,M)));

      then

       A17: (( Path_matrix (p,M)) . 2) = f by A14, A9, A10, MATRIX_3:def 7;

      3 in ( dom ( Path_matrix (p,M))) by A16;

      then

       A18: (( Path_matrix (p,M)) . 3) = g by A13, A6, A7, MATRIX_3:def 7;

      1 in ( dom ( Path_matrix (p,M))) by A16;

      then (( Path_matrix (p,M)) . 1) = b by A12, A2, A4, MATRIX_3:def 7;

      hence thesis by A15, A17, A18, FINSEQ_1: 45;

    end;

    theorem :: MATRIX_9:24

    

     Th24: for a,b,c,d,e,f,g,h,i be Element of K holds for M be Matrix of 3, K st M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*> holds for p be Element of ( Permutations 3) st p = <*2, 1, 3*> holds ( Path_matrix (p,M)) = <*b, d, i*>

    proof

      let a,b,c,d,e,f,g,h,i be Element of K;

      let M be Matrix of 3, K;

       [1, 2] in ( Indices M) by MATRIX_0: 31;

      then

      consider r be FinSequence of the carrier of K such that

       A1: r = (M . 1) and

       A2: (M * (1,2)) = (r . 2) by MATRIX_0:def 5;

      assume

       A3: M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*>;

      then (M . 1) = <*a, b, c*> by FINSEQ_1: 45;

      then

       A4: (r . 2) = b by A1, FINSEQ_1: 45;

       [3, 3] in ( Indices M) by MATRIX_0: 31;

      then

      consider z be FinSequence of the carrier of K such that

       A5: z = (M . 3) and

       A6: (M * (3,3)) = (z . 3) by MATRIX_0:def 5;

      (M . 3) = <*g, h, i*> by A3, FINSEQ_1: 45;

      then

       A7: (z . 3) = i by A5, FINSEQ_1: 45;

       [2, 1] in ( Indices M) by MATRIX_0: 31;

      then

      consider y be FinSequence of the carrier of K such that

       A8: y = (M . 2) and

       A9: (M * (2,1)) = (y . 1) by MATRIX_0:def 5;

      (M . 2) = <*d, e, f*> by A3, FINSEQ_1: 45;

      then

       A10: (y . 1) = d by A8, FINSEQ_1: 45;

      let p be Element of ( Permutations 3);

      assume

       A11: p = <*2, 1, 3*>;

      then

       A12: 2 = (p . 1) by FINSEQ_1: 45;

      

       A13: 3 = (p . 3) by A11, FINSEQ_1: 45;

      

       A14: 1 = (p . 2) by A11, FINSEQ_1: 45;

      

       A15: ( len ( Path_matrix (p,M))) = 3 by MATRIX_3:def 7;

      then

       A16: ( dom ( Path_matrix (p,M))) = ( Seg 3) by FINSEQ_1:def 3;

      then 2 in ( dom ( Path_matrix (p,M)));

      then

       A17: (( Path_matrix (p,M)) . 2) = d by A14, A9, A10, MATRIX_3:def 7;

      3 in ( dom ( Path_matrix (p,M))) by A16;

      then

       A18: (( Path_matrix (p,M)) . 3) = i by A13, A6, A7, MATRIX_3:def 7;

      1 in ( dom ( Path_matrix (p,M))) by A16;

      then (( Path_matrix (p,M)) . 1) = b by A12, A2, A4, MATRIX_3:def 7;

      hence thesis by A15, A17, A18, FINSEQ_1: 45;

    end;

    theorem :: MATRIX_9:25

    

     Th25: for a,b,c,d,e,f,g,h,i be Element of K holds for M be Matrix of 3, K st M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*> holds for p be Element of ( Permutations 3) st p = <*3, 1, 2*> holds ( Path_matrix (p,M)) = <*c, d, h*>

    proof

      let a,b,c,d,e,f,g,h,i be Element of K;

      let M be Matrix of 3, K;

       [1, 3] in ( Indices M) by MATRIX_0: 31;

      then

      consider r be FinSequence of the carrier of K such that

       A1: r = (M . 1) and

       A2: (M * (1,3)) = (r . 3) by MATRIX_0:def 5;

      assume

       A3: M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*>;

      then (M . 1) = <*a, b, c*> by FINSEQ_1: 45;

      then

       A4: (r . 3) = c by A1, FINSEQ_1: 45;

       [3, 2] in ( Indices M) by MATRIX_0: 31;

      then

      consider z be FinSequence of the carrier of K such that

       A5: z = (M . 3) and

       A6: (M * (3,2)) = (z . 2) by MATRIX_0:def 5;

      (M . 3) = <*g, h, i*> by A3, FINSEQ_1: 45;

      then

       A7: (z . 2) = h by A5, FINSEQ_1: 45;

       [2, 1] in ( Indices M) by MATRIX_0: 31;

      then

      consider y be FinSequence of the carrier of K such that

       A8: y = (M . 2) and

       A9: (M * (2,1)) = (y . 1) by MATRIX_0:def 5;

      (M . 2) = <*d, e, f*> by A3, FINSEQ_1: 45;

      then

       A10: (y . 1) = d by A8, FINSEQ_1: 45;

      let p be Element of ( Permutations 3);

      assume

       A11: p = <*3, 1, 2*>;

      then

       A12: 3 = (p . 1) by FINSEQ_1: 45;

      

       A13: 2 = (p . 3) by A11, FINSEQ_1: 45;

      

       A14: 1 = (p . 2) by A11, FINSEQ_1: 45;

      

       A15: ( len ( Path_matrix (p,M))) = 3 by MATRIX_3:def 7;

      then

       A16: ( dom ( Path_matrix (p,M))) = ( Seg 3) by FINSEQ_1:def 3;

      then 2 in ( dom ( Path_matrix (p,M)));

      then

       A17: (( Path_matrix (p,M)) . 2) = d by A14, A9, A10, MATRIX_3:def 7;

      3 in ( dom ( Path_matrix (p,M))) by A16;

      then

       A18: (( Path_matrix (p,M)) . 3) = h by A13, A6, A7, MATRIX_3:def 7;

      1 in ( dom ( Path_matrix (p,M))) by A16;

      then (( Path_matrix (p,M)) . 1) = c by A12, A2, A4, MATRIX_3:def 7;

      hence thesis by A15, A17, A18, FINSEQ_1: 45;

    end;

    theorem :: MATRIX_9:26

    

     Th26: (the multF of K $$ <*a, b, c*>) = ((a * b) * c)

    proof

      (the multF of K $$ <*a, b, c*>) = ( Product <*a, b, c*>) by GROUP_4:def 2

      .= ((a * b) * c) by FVSUM_1: 79;

      hence thesis;

    end;

    theorem :: MATRIX_9:27

    

     Th27: <*1, 3, 2*> in ( Permutations 3) & <*2, 3, 1*> in ( Permutations 3) & <*2, 1, 3*> in ( Permutations 3) & <*3, 1, 2*> in ( Permutations 3) & <*1, 2, 3*> in ( Permutations 3) & <*3, 2, 1*> in ( Permutations 3)

    proof

      set h = <*1, 2*>;

      reconsider f = <*1, 2, 3*> as one-to-one FinSequence-like Function of ( Seg 3), ( Seg 3) by FINSEQ_2: 53;

      

       A1: ( <*3*> ^ h) = <*3, 1, 2*> by FINSEQ_1: 43;

      

       A2: <*1, 3, 2*> in ( Permutations 3)

      proof

        set h = <*2, 3*>;

        ( Rev h) = <*3, 2*> by FINSEQ_5: 61;

        then

         A3: ( <*1*> ^ ( Rev h)) = <*1, 3, 2*> by FINSEQ_1: 43;

        f = ( <*1*> ^ h) & f in ( Permutations 3) by FINSEQ_1: 43, FINSEQ_2: 53, MATRIX_1:def 12;

        hence thesis by A3, Th17;

      end;

      

       A4: ( idseq 3) in ( Permutations 3) by MATRIX_1:def 12;

      then ( <*3*> ^ h) in ( Permutations 3) by Th18, FINSEQ_2: 53;

      then

       A5: ( <*3*> ^ ( Rev h)) in ( Permutations 3) by Th17;

      f = ( <*1*> ^ <*2, 3*>) & ( Rev h) = <*2, 1*> by FINSEQ_1: 43, FINSEQ_5: 61;

      hence thesis by A4, A2, A5, A1, Th5, Th15, Th18, FINSEQ_2: 53;

    end;

    

     Lm3: <*1, 2, 3*> <> <*3, 2, 1*> by FINSEQ_1: 78;

    

     Lm4: <*1, 2, 3*> <> <*1, 3, 2*> by FINSEQ_1: 78;

    

     Lm5: <*1, 2, 3*> <> <*2, 1, 3*> by FINSEQ_1: 78;

    

     Lm6: <*1, 2, 3*> <> <*2, 3, 1*> & <*1, 2, 3*> <> <*3, 1, 2*> by FINSEQ_1: 78;

    

     Lm7: <*3, 2, 1*> <> <*2, 3, 1*> & <*3, 2, 1*> <> <*3, 1, 2*> by FINSEQ_1: 78;

    

     Lm8: <*3, 2, 1*> <> <*2, 1, 3*> & <*1, 3, 2*> <> <*2, 1, 3*> by FINSEQ_1: 78;

    

     Lm9: <*1, 3, 2*> <> <*2, 3, 1*> & <*1, 3, 2*> <> <*3, 1, 2*> by FINSEQ_1: 78;

    

     Lm10: <*3, 2, 1*> <> <*1, 3, 2*> & <*2, 3, 1*> <> <*3, 1, 2*> by FINSEQ_1: 78;

    

     Lm11: <*2, 3, 1*> <> <*2, 1, 3*> & <*2, 1, 3*> <> <*3, 1, 2*> by FINSEQ_1: 78;

    theorem :: MATRIX_9:28

    

     Th28: ( <*2, 3, 1*> " ) = <*3, 1, 2*>

    proof

      set f = <*2, 3, 1*>, g = <*3, 1, 2*>;

      ( rng f) = {2, 3, 1} by FINSEQ_2: 128

      .= {1, 2, 3} by ENUMSET1: 59;

      then

       A1: ( dom f) = {1, 2, 3} & ( rng f) = ( dom g) by FINSEQ_1: 89, FINSEQ_3: 1;

      then

       A2: ( dom (g * f)) = {1, 2, 3} by RELAT_1: 27;

      

       A3: for x be object st x in ( dom (g * f)) holds ((g * f) . x) = (( id {1, 2, 3}) . x)

      proof

        let x be object;

        assume

         A4: x in ( dom (g * f));

        per cases by A2, A4, ENUMSET1:def 1;

          suppose

           A5: x = 1;

          

          then (g . (f . x)) = (g . 2) by FINSEQ_1: 45

          .= 1 by FINSEQ_1: 45

          .= (( id {1, 2, 3}) . x) by A2, A4, A5, FUNCT_1: 18;

          hence thesis by A4, FUNCT_1: 12;

        end;

          suppose

           A6: x = 2;

          

          then (g . (f . x)) = (g . 3) by FINSEQ_1: 45

          .= 2 by FINSEQ_1: 45

          .= (( id {1, 2, 3}) . x) by A2, A4, A6, FUNCT_1: 18;

          hence thesis by A4, FUNCT_1: 12;

        end;

          suppose

           A7: x = 3;

          

          then (g . (f . x)) = (g . 1) by FINSEQ_1: 45

          .= 3 by FINSEQ_1: 45

          .= (( id {1, 2, 3}) . x) by A2, A4, A7, FUNCT_1: 18;

          hence thesis by A4, FUNCT_1: 12;

        end;

      end;

      f is one-to-one & ( dom (g * f)) = ( dom ( id {1, 2, 3})) by A2, FINSEQ_3: 95, RELAT_1: 45;

      hence thesis by A1, A3, FUNCT_1: 2, FUNCT_1: 41;

    end;

    theorem :: MATRIX_9:29

    for a be Element of ( Group_of_Perm 3) st a = <*2, 3, 1*> holds (a " ) = <*3, 1, 2*>

    proof

      let a be Element of ( Group_of_Perm 3);

      reconsider a1 = a as Element of ( Permutations 3) by MATRIX_1:def 13;

      assume a = <*2, 3, 1*>;

      then (a1 " ) = <*3, 1, 2*> by Th28;

      hence thesis by MATRIX_7: 27;

    end;

    begin

    theorem :: MATRIX_9:30

    

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

    proof

      let p be Permutation of ( Seg 3);

      assume

       A1: p = <*1, 3, 2*>;

      then

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

      ex i, j st i in ( dom p) & j in ( dom p) & i <> j & (p . i) = j & (p . j) = i & for k st k <> i & k <> j & k in ( dom p) holds (p . k) = k

      proof

        take i = 2, j = 3;

        thus i in ( dom p) & j in ( dom p) by A2, ENUMSET1:def 1;

        for k st k <> i & k <> j & k in ( dom p) holds (p . k) = k

        proof

          let k;

          assume k <> i & k <> j & k in ( dom p);

          then k = 1 by A2, ENUMSET1:def 1;

          hence thesis by A1, FINSEQ_1: 45;

        end;

        hence thesis by A1, FINSEQ_1: 45;

      end;

      hence thesis by MATRIX_1:def 14;

    end;

    theorem :: MATRIX_9:31

    

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

    proof

      let p be Permutation of ( Seg 3);

      assume

       A1: p = <*2, 1, 3*>;

      then

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

      ex i, j st i in ( dom p) & j in ( dom p) & i <> j & (p . i) = j & (p . j) = i & for k st k <> i & k <> j & k in ( dom p) holds (p . k) = k

      proof

        take i = 1, j = 2;

        thus i in ( dom p) & j in ( dom p) by A2, ENUMSET1:def 1;

        for k st k <> i & k <> j & k in ( dom p) holds (p . k) = k

        proof

          let k;

          assume k <> i & k <> j & k in ( dom p);

          then k = 3 by A2, ENUMSET1:def 1;

          hence thesis by A1, FINSEQ_1: 45;

        end;

        hence thesis by A1, FINSEQ_1: 45;

      end;

      hence thesis by MATRIX_1:def 14;

    end;

    theorem :: MATRIX_9:32

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

    proof

      let p be Permutation of ( Seg 3);

      assume

       A1: p = <*3, 2, 1*>;

      then

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

      ex i, j st i in ( dom p) & j in ( dom p) & i <> j & (p . i) = j & (p . j) = i & for k st k <> i & k <> j & k in ( dom p) holds (p . k) = k

      proof

        take i = 1, j = 3;

        thus i in ( dom p) & j in ( dom p) by A2, ENUMSET1:def 1;

        for k st k <> i & k <> j & k in ( dom p) holds (p . k) = k

        proof

          let k;

          assume k <> i & k <> j & k in ( dom p);

          then k = 2 by A2, ENUMSET1:def 1;

          hence thesis by A1, FINSEQ_1: 45;

        end;

        hence thesis by A1, FINSEQ_1: 45;

      end;

      hence thesis by MATRIX_1:def 14;

    end;

    theorem :: MATRIX_9:33

    

     Th33: for p be Permutation of ( Seg n) st p = ( id ( Seg n)) holds not p is being_transposition

    proof

      let p be Permutation of ( Seg n);

      assume

       A1: p = ( id ( Seg n));

      then ( dom p) = ( Seg n) by FUNCT_1: 17;

      then not ex i, j st i in ( dom p) & j in ( dom p) & i <> j & (p . i) = j & (p . j) = i & for k st k <> i & k <> j & k in ( dom p) holds (p . k) = k by A1, FUNCT_1: 17;

      hence thesis by MATRIX_1:def 14;

    end;

    theorem :: MATRIX_9:34

    

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

    proof

      let p be Permutation of ( Seg 3);

      assume

       A1: p = <*3, 1, 2*>;

      then

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

       not ex i, j st i in ( dom p) & j in ( dom p) & i <> j & (p . i) = j & (p . j) = i & for k st k <> i & k <> j & k in ( dom p) holds (p . k) = k

      proof

        given i, j such that

         A3: i in ( dom p) and

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

         A5: for k st k <> i & k <> j & k in ( dom p) holds (p . k) = k;

        ex k be Element of NAT st k <> i & k <> j & k in ( dom p)

        proof

          

           A6: i = 1 or i = 2 or i = 3 by A2, A3, ENUMSET1:def 1;

          per cases by A2, A4, A6, ENUMSET1:def 1;

            suppose

             A7: i = 1 & j = 2;

            take 3;

            thus thesis by A2, A7, ENUMSET1:def 1;

          end;

            suppose

             A8: i = 2 & j = 3;

            take 1;

            thus thesis by A2, A8, ENUMSET1:def 1;

          end;

            suppose

             A9: i = 1 & j = 3;

            take 2;

            thus thesis by A2, A9, ENUMSET1:def 1;

          end;

            suppose

             A10: i = 2 & j = 1;

            take 3;

            thus thesis by A2, A10, ENUMSET1:def 1;

          end;

            suppose

             A11: i = 3 & j = 1;

            take 2;

            thus thesis by A2, A11, ENUMSET1:def 1;

          end;

            suppose

             A12: i = 3 & j = 2;

            take 1;

            thus thesis by A2, A12, ENUMSET1:def 1;

          end;

        end;

        then

        consider k such that

         A13: k <> i & k <> j and

         A14: k in ( dom p);

        

         A15: (p . k) = k by A5, A13, A14;

        per cases by A2, A14, ENUMSET1:def 1;

          suppose k = 1;

          hence thesis by A1, A15, FINSEQ_1: 45;

        end;

          suppose k = 2;

          hence thesis by A1, A15, FINSEQ_1: 45;

        end;

          suppose k = 3;

          hence thesis by A1, A15, FINSEQ_1: 45;

        end;

      end;

      hence thesis by MATRIX_1:def 14;

    end;

    theorem :: MATRIX_9:35

    

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

    proof

      let p be Permutation of ( Seg 3);

      assume

       A1: p = <*2, 3, 1*>;

      then

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

       not ex i, j st i in ( dom p) & j in ( dom p) & i <> j & (p . i) = j & (p . j) = i & for k st k <> i & k <> j & k in ( dom p) holds (p . k) = k

      proof

        given i, j such that

         A3: i in ( dom p) and

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

         A5: for k st k <> i & k <> j & k in ( dom p) holds (p . k) = k;

        ex k be Element of NAT st k <> i & k <> j & k in ( dom p)

        proof

          

           A6: i = 1 or i = 2 or i = 3 by A2, A3, ENUMSET1:def 1;

          per cases by A2, A4, A6, ENUMSET1:def 1;

            suppose

             A7: i = 1 & j = 2;

            take 3;

            thus thesis by A2, A7, ENUMSET1:def 1;

          end;

            suppose

             A8: i = 2 & j = 3;

            take 1;

            thus thesis by A2, A8, ENUMSET1:def 1;

          end;

            suppose

             A9: i = 1 & j = 3;

            take 2;

            thus thesis by A2, A9, ENUMSET1:def 1;

          end;

            suppose

             A10: i = 2 & j = 1;

            take 3;

            thus thesis by A2, A10, ENUMSET1:def 1;

          end;

            suppose

             A11: i = 3 & j = 1;

            take 2;

            thus thesis by A2, A11, ENUMSET1:def 1;

          end;

            suppose

             A12: i = 3 & j = 2;

            take 1;

            thus thesis by A2, A12, ENUMSET1:def 1;

          end;

        end;

        then

        consider k such that

         A13: k <> i & k <> j and

         A14: k in ( dom p);

        

         A15: (p . k) = k by A5, A13, A14;

        per cases by A2, A14, ENUMSET1:def 1;

          suppose k = 1;

          hence thesis by A1, A15, FINSEQ_1: 45;

        end;

          suppose k = 2;

          hence thesis by A1, A15, FINSEQ_1: 45;

        end;

          suppose k = 3;

          hence thesis by A1, A15, FINSEQ_1: 45;

        end;

      end;

      hence thesis by MATRIX_1:def 14;

    end;

    begin

    theorem :: MATRIX_9:36

    

     Th36: for f be Permutation of ( Seg n) holds f is FinSequence of ( Seg n)

    proof

      let f be Permutation of ( Seg n);

      

       A1: ( rng f) c= ( Seg n) by RELAT_1:def 19;

      per cases ;

        suppose n = 0 ;

        hence thesis by A1, FINSEQ_1:def 4;

      end;

        suppose n <> 0 ;

        then ( dom f) = ( Seg n) by FUNCT_2:def 1;

        then f is FinSequence by FINSEQ_1:def 2;

        hence thesis by A1, FINSEQ_1:def 4;

      end;

    end;

    theorem :: MATRIX_9:37

    

     Th37: ( <*2, 1, 3*> * <*1, 3, 2*>) = <*2, 3, 1*> & ( <*1, 3, 2*> * <*2, 1, 3*>) = <*3, 1, 2*> & ( <*2, 1, 3*> * <*3, 2, 1*>) = <*3, 1, 2*> & ( <*3, 2, 1*> * <*2, 1, 3*>) = <*2, 3, 1*> & ( <*3, 2, 1*> * <*3, 2, 1*>) = <*1, 2, 3*> & ( <*2, 1, 3*> * <*2, 1, 3*>) = <*1, 2, 3*> & ( <*1, 3, 2*> * <*1, 3, 2*>) = <*1, 2, 3*> & ( <*1, 3, 2*> * <*2, 3, 1*>) = <*3, 2, 1*> & ( <*2, 3, 1*> * <*2, 3, 1*>) = <*3, 1, 2*> & ( <*2, 3, 1*> * <*3, 1, 2*>) = <*1, 2, 3*> & ( <*3, 1, 2*> * <*2, 3, 1*>) = <*1, 2, 3*> & ( <*3, 1, 2*> * <*3, 1, 2*>) = <*2, 3, 1*> & ( <*1, 3, 2*> * <*3, 2, 1*>) = <*2, 3, 1*> & ( <*3, 2, 1*> * <*1, 3, 2*>) = <*3, 1, 2*>

    proof

      set F = <*2, 3, 1*>, G = <*3, 1, 2*>;

      set f = <*1, 3, 2*>, g = <*2, 1, 3*>, h = <*3, 2, 1*>;

      

       A1: ( dom f) = {1, 2, 3} by FINSEQ_1: 89, FINSEQ_3: 1;

      then

       A2: 1 in ( dom f) by ENUMSET1:def 1;

      

       A3: f is Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

      

       A4: g is Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

      

       A5: 2 in ( dom f) by A1, ENUMSET1:def 1;

      

       A6: ( dom G) = {1, 2, 3} by FINSEQ_1: 89, FINSEQ_3: 1;

      then

       A7: 1 in ( dom G) by ENUMSET1:def 1;

      

       A8: 3 in ( dom G) by A6, ENUMSET1:def 1;

      

       A9: 2 in ( dom G) by A6, ENUMSET1:def 1;

      

       A10: 3 in ( dom f) by A1, ENUMSET1:def 1;

      

       A11: ( dom g) = {1, 2, 3} by FINSEQ_1: 89, FINSEQ_3: 1;

      then

       A12: 1 in ( dom g) by ENUMSET1:def 1;

      

       A13: 3 in ( dom g) by A11, ENUMSET1:def 1;

      

       A14: 2 in ( dom g) by A11, ENUMSET1:def 1;

      

       A15: ( dom h) = {1, 2, 3} by FINSEQ_1: 89, FINSEQ_3: 1;

      then

       A16: 1 in ( dom h) by ENUMSET1:def 1;

      

       A17: 3 in ( dom h) by A15, ENUMSET1:def 1;

      

       A18: 2 in ( dom h) by A15, ENUMSET1:def 1;

      

       A19: f is Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

      

       A20: G is Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

      

       A21: ( dom F) = {1, 2, 3} by FINSEQ_1: 89, FINSEQ_3: 1;

      then

       A22: 1 in ( dom F) by ENUMSET1:def 1;

      

       A23: 3 in ( dom F) by A21, ENUMSET1:def 1;

      

       A24: 2 in ( dom F) by A21, ENUMSET1:def 1;

      

       A25: h is Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

      

       A26: F is Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

      then

      reconsider f, g, h, F, G as FinSequence of ( Seg 3) by A4, A25, A20, A19, Th36;

      

       A27: 3 = ( len g) by FINSEQ_1: 45;

      then

      reconsider gf = (g * f) as FinSequence of ( Seg 3) by A3, FINSEQ_2: 46;

      

       A28: (gf . 1) = (g . (f . 1)) by A2, FUNCT_1: 13

      .= (g . 1) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      

       A29: g is Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

      then

      reconsider gg = (g * g) as FinSequence of ( Seg 3) by A27, FINSEQ_2: 46;

      

       A30: (gg . 1) = (g . (g . 1)) by A12, FUNCT_1: 13

      .= (g . 2) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      

       A31: 3 = ( len f) by FINSEQ_1: 45;

      then

      reconsider fg = (f * g) as FinSequence of ( Seg 3) by A4, FINSEQ_2: 46;

      

       A32: (fg . 2) = (f . (g . 2)) by A14, FUNCT_1: 13

      .= (f . 1) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      

       A33: (gf . 3) = (g . (f . 3)) by A10, FUNCT_1: 13

      .= (g . 2) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      

       A34: (gf . 2) = (g . (f . 2)) by A5, FUNCT_1: 13

      .= (g . 3) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A35: f is Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

      then

      reconsider ff = (f * f) as FinSequence of ( Seg 3) by A31, FINSEQ_2: 46;

      ( len gf) = 3 by A27, A35, FINSEQ_2: 43;

      hence ( <*2, 1, 3*> * <*1, 3, 2*>) = <*2, 3, 1*> by A28, A34, A33, FINSEQ_1: 45;

      

       A36: (fg . 1) = (f . (g . 1)) by A12, FUNCT_1: 13

      .= (f . 2) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A37: (fg . 3) = (f . (g . 3)) by A13, FUNCT_1: 13

      .= (f . 3) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      ( len fg) = 3 by A31, A29, FINSEQ_2: 43;

      hence ( <*1, 3, 2*> * <*2, 1, 3*>) = <*3, 1, 2*> by A36, A32, A37, FINSEQ_1: 45;

      

       A38: (ff . 2) = (f . (f . 2)) by A5, FUNCT_1: 13

      .= (f . 3) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      

       A39: (gg . 3) = (g . (g . 3)) by A13, FUNCT_1: 13

      .= (g . 3) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A40: (gg . 2) = (g . (g . 2)) by A14, FUNCT_1: 13

      .= (g . 1) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      

       A41: h is Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

      then

      reconsider gh = (g * h) as FinSequence of ( Seg 3) by A27, FINSEQ_2: 46;

      

       A42: (gh . 1) = (g . (h . 1)) by A16, FUNCT_1: 13

      .= (g . 3) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A43: (gh . 3) = (g . (h . 3)) by A17, FUNCT_1: 13

      .= (g . 1) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      

       A44: (gh . 2) = (g . (h . 2)) by A18, FUNCT_1: 13

      .= (g . 2) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      

       A45: 3 = ( len h) by FINSEQ_1: 45;

      then

      reconsider hf = (h * f) as FinSequence of ( Seg 3) by A19, FINSEQ_2: 46;

      reconsider hh = (h * h) as FinSequence of ( Seg 3) by A45, A41, FINSEQ_2: 46;

      

       A46: (hh . 1) = (h . (h . 1)) by A16, FUNCT_1: 13

      .= (h . 3) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      reconsider fh = (f * h) as FinSequence of ( Seg 3) by A25, A31, FINSEQ_2: 46;

      

       A47: (fh . 1) = (f . (h . 1)) by A16, FUNCT_1: 13

      .= (f . 3) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      

       A48: (fh . 3) = (f . (h . 3)) by A17, FUNCT_1: 13

      .= (f . 1) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      reconsider fF = (f * F) as FinSequence of ( Seg 3) by A26, A31, FINSEQ_2: 46;

      

       A49: (fF . 1) = (f . (F . 1)) by A22, FUNCT_1: 13

      .= (f . 2) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A50: (fF . 2) = (f . (F . 2)) by A24, FUNCT_1: 13

      .= (f . 3) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      reconsider hg = (h * g) as FinSequence of ( Seg 3) by A45, A29, FINSEQ_2: 46;

      

       A51: (hg . 1) = (h . (g . 1)) by A12, FUNCT_1: 13

      .= (h . 2) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      

       A52: (hg . 2) = (h . (g . 2)) by A14, FUNCT_1: 13

      .= (h . 1) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A53: (hh . 3) = (h . (h . 3)) by A17, FUNCT_1: 13

      .= (h . 1) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A54: (hh . 2) = (h . (h . 2)) by A18, FUNCT_1: 13

      .= (h . 2) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      ( len gh) = 3 by A27, A41, FINSEQ_2: 43;

      hence ( <*2, 1, 3*> * <*3, 2, 1*>) = <*3, 1, 2*> by A42, A44, A43, FINSEQ_1: 45;

      

       A55: (ff . 3) = (f . (f . 3)) by A10, FUNCT_1: 13

      .= (f . 2) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A56: (hg . 3) = (h . (g . 3)) by A13, FUNCT_1: 13

      .= (h . 3) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      ( len hg) = 3 by A45, A29, FINSEQ_2: 43;

      hence ( <*3, 2, 1*> * <*2, 1, 3*>) = <*2, 3, 1*> by A51, A52, A56, FINSEQ_1: 45;

      ( len hh) = 3 by A45, A41, FINSEQ_2: 43;

      hence ( <*3, 2, 1*> * <*3, 2, 1*>) = <*1, 2, 3*> by A46, A54, A53, FINSEQ_1: 45;

      ( len gg) = 3 by A27, A29, FINSEQ_2: 43;

      hence ( <*2, 1, 3*> * <*2, 1, 3*>) = <*1, 2, 3*> by A30, A40, A39, FINSEQ_1: 45;

      

       A57: (ff . 1) = (f . (f . 1)) by A2, FUNCT_1: 13

      .= (f . 1) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      

       A58: (fF . 3) = (f . (F . 3)) by A23, FUNCT_1: 13

      .= (f . 1) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      ( len ff) = 3 by A31, A35, FINSEQ_2: 43;

      hence ( <*1, 3, 2*> * <*1, 3, 2*>) = <*1, 2, 3*> by A57, A38, A55, FINSEQ_1: 45;

      

       A59: F is Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

      then ( len fF) = 3 by A31, FINSEQ_2: 43;

      hence ( <*1, 3, 2*> * <*2, 3, 1*>) = <*3, 2, 1*> by A49, A50, A58, FINSEQ_1: 45;

      

       A60: (fh . 2) = (f . (h . 2)) by A18, FUNCT_1: 13

      .= (f . 2) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A61: 3 = ( len F) by FINSEQ_1: 45;

      then

      reconsider FF = (F * F) as FinSequence of ( Seg 3) by A26, FINSEQ_2: 46;

      reconsider FG = (F * G) as FinSequence of ( Seg 3) by A20, A61, FINSEQ_2: 46;

      

       A62: (FG . 1) = (F . (G . 1)) by A7, FUNCT_1: 13

      .= (F . 3) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      

       A63: (FG . 2) = (F . (G . 2)) by A9, FUNCT_1: 13

      .= (F . 1) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      

       A64: (FF . 3) = (F . (F . 3)) by A23, FUNCT_1: 13

      .= (F . 1) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      

       A65: (FG . 3) = (F . (G . 3)) by A8, FUNCT_1: 13

      .= (F . 2) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A66: (FF . 2) = (F . (F . 2)) by A24, FUNCT_1: 13

      .= (F . 3) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      

       A67: (FF . 1) = (F . (F . 1)) by A22, FUNCT_1: 13

      .= (F . 2) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A68: 3 = ( len G) by FINSEQ_1: 45;

      then

      reconsider GF = (G * F) as FinSequence of ( Seg 3) by A26, FINSEQ_2: 46;

      reconsider GG = (G * G) as FinSequence of ( Seg 3) by A20, A68, FINSEQ_2: 46;

      

       A69: (GG . 1) = (G . (G . 1)) by A7, FUNCT_1: 13

      .= (G . 3) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      

       A70: (GG . 2) = (G . (G . 2)) by A9, FUNCT_1: 13

      .= (G . 1) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A71: (GF . 3) = (G . (F . 3)) by A23, FUNCT_1: 13

      .= (G . 1) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      

       A72: (GG . 3) = (G . (G . 3)) by A8, FUNCT_1: 13

      .= (G . 2) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      

       A73: (GF . 2) = (G . (F . 2)) by A24, FUNCT_1: 13

      .= (G . 3) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      

       A74: (GF . 1) = (G . (F . 1)) by A22, FUNCT_1: 13

      .= (G . 2) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      ( len FF) = 3 by A61, A59, FINSEQ_2: 43;

      hence ( <*2, 3, 1*> * <*2, 3, 1*>) = <*3, 1, 2*> by A67, A66, A64, FINSEQ_1: 45;

      

       A75: G is Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

      then ( len FG) = 3 by A61, FINSEQ_2: 43;

      hence ( <*2, 3, 1*> * <*3, 1, 2*>) = <*1, 2, 3*> by A62, A63, A65, FINSEQ_1: 45;

      

       A76: (hf . 3) = (h . (f . 3)) by A10, FUNCT_1: 13

      .= (h . 2) by FINSEQ_1: 45

      .= 2 by FINSEQ_1: 45;

      ( len GF) = 3 by A68, A59, FINSEQ_2: 43;

      hence ( <*3, 1, 2*> * <*2, 3, 1*>) = <*1, 2, 3*> by A74, A73, A71, FINSEQ_1: 45;

      ( len GG) = 3 by A68, A75, FINSEQ_2: 43;

      hence ( <*3, 1, 2*> * <*3, 1, 2*>) = <*2, 3, 1*> by A69, A70, A72, FINSEQ_1: 45;

      

       A77: (hf . 2) = (h . (f . 2)) by A5, FUNCT_1: 13

      .= (h . 3) by FINSEQ_1: 45

      .= 1 by FINSEQ_1: 45;

      ( len fh) = 3 by A31, A41, FINSEQ_2: 43;

      hence ( <*1, 3, 2*> * <*3, 2, 1*>) = <*2, 3, 1*> by A47, A60, A48, FINSEQ_1: 45;

      

       A78: (hf . 1) = (h . (f . 1)) by A2, FUNCT_1: 13

      .= (h . 1) by FINSEQ_1: 45

      .= 3 by FINSEQ_1: 45;

      ( len hf) = 3 by A45, A35, FINSEQ_2: 43;

      hence ( <*3, 2, 1*> * <*1, 3, 2*>) = <*3, 1, 2*> by A78, A77, A76, FINSEQ_1: 45;

    end;

    theorem :: MATRIX_9:38

    

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

    proof

      let p be Permutation of ( Seg 3);

      p in ( Permutations 3) by MATRIX_1:def 12;

      then

       A1: p = <*1, 2, 3*> or p = <*2, 1, 3*> or p = <*2, 3, 1*> or p = <*3, 1, 2*> or p = <*3, 2, 1*> or p = <*1, 3, 2*> by Th19, ENUMSET1:def 4;

      assume p is being_transposition;

      hence thesis by A1, Th33, Th34, Th35, FINSEQ_2: 53;

    end;

    theorem :: MATRIX_9:39

    

     Th39: for f,g be Element of ( Permutations n) holds (f * g) in ( Permutations n)

    proof

      let f,g be Element of ( Permutations n);

      reconsider F = f, G = g as Permutation of ( Seg n) by MATRIX_1:def 12;

      (F * G) is Permutation of ( Seg n);

      hence thesis by MATRIX_1:def 12;

    end;

    

     Lm12: <*1, 2, 3*> is even Permutation of ( Seg 3) by FINSEQ_2: 53, MATRIX_1: 16;

    

     Lm13: <*2, 3, 1*> is even Permutation of ( Seg 3)

    proof

      reconsider f = <*2, 3, 1*> as Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

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

      proof

        reconsider l1 = <*2, 1, 3*>, l2 = <*1, 3, 2*> as Element of ( Group_of_Perm 3) by Th27, MATRIX_1:def 13;

        reconsider l = <*l2, l1*> as FinSequence of ( Group_of_Perm 3);

        take l;

        

         A1: ( len l) = (2 * 1) by FINSEQ_1: 44;

        hence (( len l) mod 2) = 0 by NAT_D: 13;

        reconsider L2 = l2, L1 = l1 as Element of ( Permutations 3) by Th27;

        ( Product l) = (l2 * l1) by GROUP_4: 10

        .= (L1 * L2) by MATRIX_1:def 13

        .= <*2, 3, 1*> by Th37;

        hence f = ( Product l);

        

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

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

        proof

          let i;

          assume

           A3: i in ( dom l);

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

            suppose

             A4: i = 2;

            then

            reconsider q = (l . i) as Element of ( Permutations 3) by Th27, FINSEQ_1: 44;

            

             A5: ( len ( Permutations 3)) = 3 by MATRIX_1: 9;

            (l . i) = <*2, 1, 3*> by A4, FINSEQ_1: 44;

            then q is being_transposition by A5, Th31;

            hence thesis;

          end;

            suppose

             A6: i = 1;

            then

            reconsider q = (l . i) as Element of ( Permutations 3) by Th27, FINSEQ_1: 44;

            

             A7: ( len ( Permutations 3)) = 3 by MATRIX_1: 9;

            (l . i) = <*1, 3, 2*> by A6, FINSEQ_1: 44;

            then q is being_transposition by A7, Th30;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis by MATRIX_1:def 15;

    end;

    

     Lm14: <*3, 1, 2*> is even Permutation of ( Seg 3)

    proof

      reconsider f = <*3, 1, 2*> as Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

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

      proof

        reconsider l1 = <*2, 1, 3*>, l2 = <*1, 3, 2*> as Element of ( Group_of_Perm 3) by Th27, MATRIX_1:def 13;

        reconsider l = <*l1, l2*> as FinSequence of ( Group_of_Perm 3);

        take l;

        

         A1: ( len l) = (2 * 1) by FINSEQ_1: 44;

        hence (( len l) mod 2) = 0 by NAT_D: 13;

        reconsider L2 = l2, L1 = l1 as Element of ( Permutations 3) by Th27;

        ( Product l) = (l1 * l2) by GROUP_4: 10

        .= (L2 * L1) by MATRIX_1:def 13

        .= <*3, 1, 2*> by Th37;

        hence f = ( Product l);

        

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

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

        proof

          let i;

          assume

           A3: i in ( dom l);

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

            suppose

             A4: i = 2;

            then

            reconsider q = (l . i) as Element of ( Permutations 3) by Th27, FINSEQ_1: 44;

            

             A5: ( len ( Permutations 3)) = 3 by MATRIX_1: 9;

            (l . i) = <*1, 3, 2*> by A4, FINSEQ_1: 44;

            then q is being_transposition by A5, Th30;

            hence thesis;

          end;

            suppose

             A6: i = 1;

            then

            reconsider q = (l . i) as Element of ( Permutations 3) by Th27, FINSEQ_1: 44;

            

             A7: ( len ( Permutations 3)) = 3 by MATRIX_1: 9;

            (l . i) = <*2, 1, 3*> by A6, FINSEQ_1: 44;

            then q is being_transposition by A7, Th31;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis by MATRIX_1:def 15;

    end;

    theorem :: MATRIX_9:40

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

    proof

      let l be FinSequence of ( Group_of_Perm n);

      ( Product l) in the carrier of ( Group_of_Perm n);

      then ( Product l) in ( Permutations n) by MATRIX_1:def 13;

      then

      reconsider Pf = ( Product l) as Permutation of ( Seg n) by MATRIX_1:def 12;

      assume

       A1: (( len l) mod 2) = 0 & for i be Element of NAT st i in ( dom l) holds ex q be Element of ( Permutations n) st (l . i) = q & q is being_transposition;

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

      proof

        consider l be FinSequence of the carrier of ( Group_of_Perm n) such that

         A2: (( len l) mod 2) = 0 & Pf = ( Product l) and

         A3: for i be Element of NAT st i in ( dom l) holds ex q be Element of ( Permutations n) st (l . i) = q & q is being_transposition by A1;

        take l;

        thus (( len l) mod 2) = 0 & Pf = ( Product l) by A2;

        let i;

        thus thesis by A3;

      end;

      hence thesis by MATRIX_1:def 15;

    end;

    

     Lm15: for p be Permutation of ( Seg 3) holds (p * <*1, 2, 3*>) = p

    proof

      let p be Permutation of ( Seg 3);

      p is Element of ( Permutations 3) by MATRIX_1:def 12;

      hence thesis by FINSEQ_2: 53, MATRIX_1: 12;

    end;

    

     Lm16: for p be Permutation of ( Seg 3) holds ( <*1, 2, 3*> * p) = p

    proof

      let p be Permutation of ( Seg 3);

      p is Element of ( Permutations 3) by MATRIX_1:def 12;

      hence thesis by FINSEQ_2: 53, MATRIX_1: 12;

    end;

    theorem :: MATRIX_9:41

    

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

    proof

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

      let l be FinSequence of ( Group_of_Perm 3);

      assume that

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

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

      

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

      proof

        let k be Nat;

        assume

         A4: P[k];

        let f be FinSequence of ( Group_of_Perm 3);

        assume that

         A5: ( len f) = (2 * (k + 1)) and

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

        reconsider k as Element of NAT by ORDINAL1:def 12;

        set l = (2 * k);

        

         A7: 1 <= (l + 1) by NAT_1: 11;

        ( rng (f | ( Seg (2 * k)))) c= the carrier of ( Group_of_Perm 3) by RELAT_1:def 19;

        then

        reconsider g = (f | ( Seg (2 * k))) as FinSequence of ( Group_of_Perm 3) by FINSEQ_1:def 4;

        

         A8: l <= (l + 1) by NAT_1: 11;

        

         A9: ((f | ( Seg (l + 1))) | ( Seg l)) = ((f | (l + 1)) | l)

        .= (f | l) by A8, FINSEQ_5: 77

        .= (f | ( Seg l));

        

         A10: ( dom g) c= ( dom f) by RELAT_1: 60;

        

         A11: for i be Element of NAT st i in ( dom g) holds ex q be Element of ( Permutations 3) st (g . i) = q & q is being_transposition

        proof

          let i be Element of NAT ;

          assume

           A12: i in ( dom g);

          then

          consider q be Element of ( Permutations 3) such that

           A13: (f . i) = q & q is being_transposition by A6, A10;

          take q;

          thus thesis by A12, A13, FUNCT_1: 47;

        end;

        set h = (f | ( Seg (l + 1)));

        ( len f) = ((l + 1) + 1) by A5;

        then ( len h) = (l + 1) by FINSEQ_3: 53;

        then

         A14: h = ((h | ( Seg l)) ^ <*(h . (l + 1))*>) by FINSEQ_3: 55;

        

         A15: ( dom f) = ( Seg (2 * (k + 1))) by A5, FINSEQ_1:def 3;

        (l + 1) <= (l + 2) by XREAL_1: 6;

        then 1 <= (l + 2) by A7, XXREAL_0: 2;

        then

         A16: (l + 2) in ( dom f) by A15;

        then

        consider q1 be Element of ( Permutations 3) such that

         A17: (f . (l + 2)) = q1 and

         A18: q1 is being_transposition by A6;

        

         A19: (f . ((l + 1) + 1)) = (f /. (l + 2)) by A16, PARTFUN1:def 6;

        (l + 1) <= (l + 2) by XREAL_1: 6;

        then

         A20: (l + 1) in ( dom f) by A15, A7;

        then

        consider q2 be Element of ( Permutations 3) such that

         A21: (f . (l + 1)) = q2 and

         A22: q2 is being_transposition by A6;

        reconsider q12 = (q1 * q2) as Element of ( Permutations 3) by Th39;

        (h . (l + 1)) = (f . (l + 1)) by FINSEQ_1: 4, FUNCT_1: 49;

        then

         A23: (h . (l + 1)) = (f /. (l + 1)) by A20, PARTFUN1:def 6;

        f = ((f | ( Seg (l + 1))) ^ <*(f . ((l + 1) + 1))*>) by A5, FINSEQ_3: 55;

        then f = (g ^ ( <*(f /. (l + 1))*> ^ <*(f /. (l + 2))*>)) by A14, A9, A23, A19, FINSEQ_1: 32;

        

        then

         A24: ( Product f) = (( Product g) * ( Product ( <*(f /. (l + 1))*> ^ <*(f /. (l + 2))*>))) by GROUP_4: 5

        .= (( Product g) * (( Product <*(f /. (l + 1))*>) * (f /. (l + 2)))) by GROUP_4: 6

        .= (( Product g) * ((f /. (l + 1)) * (f /. (l + 2)))) by GROUP_4: 9;

        reconsider Pg = ( Product g) as Element of ( Permutations 3) by MATRIX_1:def 13;

        ( Product g) in the carrier of ( Group_of_Perm 3);

        then ( Product g) in ( Permutations 3) by MATRIX_1:def 13;

        then

         A25: ( Product g) is Permutation of ( Seg 3) by MATRIX_1:def 12;

        

         A26: ( len ( Permutations 3)) = 3 by MATRIX_1: 9;

        then

         A27: q1 = <*2, 1, 3*> or q1 = <*1, 3, 2*> or q1 = <*3, 2, 1*> by A18, Th38;

        

         A28: q1 = (f /. (l + 2)) by A16, A17, PARTFUN1:def 6;

        (q1 * q2) in ( Permutations 3) by Th39;

        then

         A29: (q1 * q2) is Permutation of ( Seg 3) by MATRIX_1:def 12;

        q2 = (f /. (l + 1)) by A20, A21, PARTFUN1:def 6;

        then

         A30: ((f /. (l + 1)) * (f /. (l + 2))) = (q1 * q2) by A28, MATRIX_7: 9;

        then

         A31: ( Product f) = (q12 * Pg) by A24, MATRIX_7: 9;

        (2 * k) <= ((2 * k) + 2) by NAT_1: 11;

        then ( Seg (2 * k)) c= ( Seg (2 * (k + 1))) by FINSEQ_1: 5;

        then ( dom g) = ( Seg (2 * k)) by A15, RELAT_1: 62;

        then

         A32: ( len g) = (2 * k) by FINSEQ_1:def 3;

        then

         A33: ( Product g) = <*1, 2, 3*> or ( Product g) = <*2, 3, 1*> or ( Product g) = <*3, 1, 2*> by A4, A11;

        ( Product f) = <*1, 2, 3*> or ( Product f) = <*2, 3, 1*> or ( Product f) = <*3, 1, 2*>

        proof

          per cases by A4, A32, A11, A22, A26, A27, Th37, Th38;

            suppose Pg = <*1, 2, 3*> & (q1 * q2) = <*2, 3, 1*>;

            hence thesis by A29, A31, Lm15;

          end;

            suppose Pg = <*2, 3, 1*> & (q1 * q2) = <*2, 3, 1*>;

            hence thesis by A24, A30, Th37, MATRIX_7: 9;

          end;

            suppose Pg = <*2, 3, 1*> & (q1 * q2) = <*3, 1, 2*>;

            hence thesis by A31, Th37;

          end;

            suppose (q1 * q2) = <*1, 2, 3*>;

            hence thesis by A33, A25, A31, Lm16;

          end;

            suppose Pg = <*1, 2, 3*> & (q1 * q2) = <*3, 1, 2*>;

            hence thesis by A29, A31, Lm15;

          end;

            suppose Pg = <*3, 1, 2*> & (q1 * q2) = <*2, 3, 1*>;

            hence thesis by A31, Th37;

          end;

            suppose Pg = <*3, 1, 2*> & (q1 * q2) = <*3, 1, 2*>;

            hence thesis by A24, A30, Th37, MATRIX_7: 9;

          end;

        end;

        hence thesis;

      end;

      

       A34: P[ 0 ]

      proof

        set G = ( Group_of_Perm 3);

        let f be FinSequence of ( Group_of_Perm 3);

        assume that

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

        

         A36: ( 1_ G) = <*1, 2, 3*> by FINSEQ_2: 53, MATRIX_1: 15;

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

        hence thesis by A36, GROUP_4: 8;

      end;

      

       A37: for s be Nat holds P[s] from NAT_1:sch 2( A34, A3);

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

      hence thesis by A2, A37;

    end;

    

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

    proof

      let l be FinSequence of ( Group_of_Perm 3) such that

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

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

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

      hence thesis by A1, Th41;

    end;

    registration

      cluster odd for Permutation of ( Seg 3);

      existence

      proof

        reconsider f = <*3, 2, 1*> as Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

         not ex l be FinSequence of ( Group_of_Perm 3) st (( len l) mod 2) = 0 & f = ( Product l) & for i st i in ( dom l) holds ex q be Element of ( Permutations 3) st (l . i) = q & q is being_transposition by Lm3, Lm7, Lm17;

        then f is odd by MATRIX_1:def 15;

        hence thesis;

      end;

    end

    theorem :: MATRIX_9:42

    

     Th42: <*3, 2, 1*> is odd Permutation of ( Seg 3)

    proof

      reconsider f = <*3, 2, 1*> as Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

       not ex l be FinSequence of ( Group_of_Perm 3) st (( len l) mod 2) = 0 & f = ( Product l) & for i st i in ( dom l) holds ex q be Element of ( Permutations 3) st (l . i) = q & q is being_transposition by Lm3, Lm7, Lm17;

      hence thesis by MATRIX_1:def 15;

    end;

    theorem :: MATRIX_9:43

    

     Th43: <*2, 1, 3*> is odd Permutation of ( Seg 3)

    proof

      reconsider f = <*2, 1, 3*> as Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

       not ex l be FinSequence of ( Group_of_Perm 3) st (( len l) mod 2) = 0 & f = ( Product l) & for i st i in ( dom l) holds ex q be Element of ( Permutations 3) st (l . i) = q & q is being_transposition by Lm5, Lm11, Lm17;

      hence thesis by MATRIX_1:def 15;

    end;

    theorem :: MATRIX_9:44

    

     Th44: <*1, 3, 2*> is odd Permutation of ( Seg 3)

    proof

      reconsider f = <*1, 3, 2*> as Permutation of ( Seg 3) by Th27, MATRIX_1:def 12;

       not ex l be FinSequence of ( Group_of_Perm 3) st (( len l) mod 2) = 0 & f = ( Product l) & for i st i in ( dom l) holds ex q be Element of ( Permutations 3) st (l . i) = q & q is being_transposition by Lm4, Lm9, Lm17;

      hence thesis by MATRIX_1:def 15;

    end;

    theorem :: MATRIX_9:45

    for p be odd Permutation of ( Seg 3) holds p = <*3, 2, 1*> or p = <*1, 3, 2*> or p = <*2, 1, 3*>

    proof

      let p be odd Permutation of ( Seg 3);

      p in ( Permutations 3) by MATRIX_1:def 12;

      hence thesis by Lm12, Lm13, Lm14, Th19, ENUMSET1:def 4;

    end;

    begin

    theorem :: MATRIX_9:46

    for a,b,c,d,e,f,g,h,i be Element of K holds for M be Matrix of 3, K st M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*> holds ( Det M) = (((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h))

    proof

      reconsider a3 = <*1, 3, 2*>, a4 = <*2, 3, 1*>, a5 = <*2, 1, 3*>, a6 = <*3, 1, 2*> as Element of ( Permutations 3) by Th27;

      reconsider id3 = ( idseq 3) as Permutation of ( Seg 3);

      reconsider Id3 = ( idseq 3) as Element of ( Permutations 3) by MATRIX_1:def 12;

      

       A1: id3 is even by MATRIX_1: 16;

      reconsider rid3 = ( Rev ( idseq 3)) as Element of ( Permutations 3) by Th4;

      let a,b,c,d,e,f,g,h,i be Element of K;

      let M be Matrix of 3, K;

      assume

       A2: M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*>;

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

      then ( In (( Permutations 3),( Fin ( Permutations 3)))) = ( Permutations 3) by SUBSET_1:def 8;

      then

      reconsider X = {Id3, rid3, a3, a4, a5, a6} as Element of ( Fin ( Permutations 3)) by Th15, Th19, FINSEQ_2: 53;

      reconsider B1 = {.Id3, rid3, a3.}, B2 = {.a4, a5, a6.} as Element of ( Fin ( Permutations 3));

      set F = the addF of K;

      

       A3: ( In (( Permutations 3),( Fin ( Permutations 3)))) = X & X = ( {Id3, rid3, a3} \/ {a4, a5, a6}) by Th15, Th19, ENUMSET1: 13, FINSEQ_2: 53;

      now

        let x be object;

        assume

         A4: x in B1;

        then x = Id3 or x = rid3 or x = a3 by ENUMSET1:def 1;

        then not x in B2 by Lm5, Lm6, Lm7, Lm8, Lm9, Th15, ENUMSET1:def 1, FINSEQ_2: 53;

        hence x in (B1 \ B2) by A4, XBOOLE_0:def 5;

      end;

      then

       A5: B1 c= (B1 \ B2) by TARSKI:def 3;

      for x be object st x in (B1 \ B2) holds x in B1 by XBOOLE_0:def 5;

      then (B1 \ B2) c= B1 by TARSKI:def 3;

      then (B1 \ B2) = B1 by A5, XBOOLE_0:def 10;

      then

       A6: B1 misses B2 by XBOOLE_1: 83;

      set r = ( Path_product M);

      

       A7: 3 = ( len ( Permutations 3)) by MATRIX_1: 9;

      then Id3 is even by MATRIX_1: 16;

      then

      reconsider r1 = (r . id3), r2 = (r . rid3), r3 = (r . a3), r4 = (r . a4), r5 = (r . a5), r6 = (r . a6) as Element of K by FUNCT_2: 5;

      

       A8: (r . id3) = ( - ((the multF of K $$ ( Path_matrix (Id3,M))),Id3)) by MATRIX_3:def 8

      .= (the multF of K $$ ( Path_matrix (Id3,M))) by A1, A7, MATRIX_1:def 16

      .= (the multF of K $$ <*a, e, i*>) by A2, Th20, FINSEQ_2: 53

      .= ((a * e) * i) by Th26;

      

       A9: (r . a6) = ( - ((the multF of K $$ ( Path_matrix (a6,M))),a6)) by MATRIX_3:def 8

      .= (the multF of K $$ ( Path_matrix (a6,M))) by A7, Lm14, MATRIX_1:def 16

      .= (the multF of K $$ <*c, d, h*>) by A2, Th25

      .= ((c * d) * h) by Th26;

      

       A10: (r . a5) = ( - ((the multF of K $$ ( Path_matrix (a5,M))),a5)) by MATRIX_3:def 8

      .= ( - (the multF of K $$ ( Path_matrix (a5,M)))) by A7, Th43, MATRIX_1:def 16

      .= ( - (the multF of K $$ <*b, d, i*>)) by A2, Th24

      .= ( - ((b * d) * i)) by Th26;

      

       A11: (r . a4) = ( - ((the multF of K $$ ( Path_matrix (a4,M))),a4)) by MATRIX_3:def 8

      .= (the multF of K $$ ( Path_matrix (a4,M))) by A7, Lm13, MATRIX_1:def 16

      .= (the multF of K $$ <*b, f, g*>) by A2, Th23

      .= ((b * f) * g) by Th26;

      

       A12: (r . a3) = ( - ((the multF of K $$ ( Path_matrix (a3,M))),a3)) by MATRIX_3:def 8

      .= ( - (the multF of K $$ ( Path_matrix (a3,M)))) by A7, Th44, MATRIX_1:def 16

      .= ( - (the multF of K $$ <*a, f, h*>)) by A2, Th22

      .= ( - ((a * f) * h)) by Th26;

      

       A13: (r . rid3) = ( - ((the multF of K $$ ( Path_matrix (rid3,M))),rid3)) by MATRIX_3:def 8

      .= ( - (the multF of K $$ ( Path_matrix (rid3,M)))) by A7, Th15, Th42, MATRIX_1:def 16

      .= ( - (the multF of K $$ <*c, e, g*>)) by A2, Th15, Th21

      .= ( - ((c * e) * g)) by Th26;

      

       A14: (F $$ (B1,r)) = ((r1 + r2) + r3) & (F $$ (B2,r)) = ((r4 + r5) + r6) by Lm3, Lm4, Lm10, Lm11, Th15, FINSEQ_2: 53, SETWOP_2: 3;

      ( Det M) = (F $$ (( In (( Permutations 3),( Fin ( Permutations 3)))),r)) by MATRIX_3:def 9

      .= (F . ((F $$ (B1,r)),(F $$ (B2,r)))) by A3, A6, SETWOP_2: 4

      .= (((r1 + r2) + r3) + (r4 + (r5 + r6))) by A14, RLVECT_1:def 3

      .= ((((r1 + r2) + r3) + r4) + (r5 + r6)) by RLVECT_1:def 3

      .= (((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)) by A8, A13, A12, A11, A10, A9, RLVECT_1:def 3;

      hence thesis;

    end;

    theorem :: MATRIX_9:47

    for a,b,c,d,e,f,g,h,i be Element of K holds for M be Matrix of 3, K st M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*> holds ( Per M) = (((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h))

    proof

      reconsider rid3 = ( Rev ( idseq 3)) as Element of ( Permutations 3) by Th4;

      let a,b,c,d,e,f,g,h,i be Element of K;

      let M be Matrix of 3, K;

      assume

       A1: M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*>;

      reconsider a3 = <*1, 3, 2*>, a4 = <*2, 3, 1*>, a5 = <*2, 1, 3*>, a6 = <*3, 1, 2*> as Element of ( Permutations 3) by Th27;

      reconsider id3 = ( idseq 3) as Permutation of ( Seg 3);

      reconsider Id3 = ( idseq 3) as Element of ( Permutations 3) by MATRIX_1:def 12;

      reconsider B1 = {.Id3, rid3, a3.}, B2 = {.a4, a5, a6.} as Element of ( Fin ( Permutations 3));

      set r = ( PPath_product M);

      

       A2: (r . id3) = (the multF of K $$ ( Path_matrix (Id3,M))) by Def1

      .= (the multF of K $$ <*a, e, i*>) by A1, Th20, FINSEQ_2: 53

      .= ((a * e) * i) by Th26;

      

       A3: (r . a6) = (the multF of K $$ ( Path_matrix (a6,M))) by Def1

      .= (the multF of K $$ <*c, d, h*>) by A1, Th25

      .= ((c * d) * h) by Th26;

      

       A4: (r . a5) = (the multF of K $$ ( Path_matrix (a5,M))) by Def1

      .= (the multF of K $$ <*b, d, i*>) by A1, Th24

      .= ((b * d) * i) by Th26;

      

       A5: (r . a4) = (the multF of K $$ ( Path_matrix (a4,M))) by Def1

      .= (the multF of K $$ <*b, f, g*>) by A1, Th23

      .= ((b * f) * g) by Th26;

      now

        let x be object;

        assume

         A6: x in B1;

        then x = Id3 or x = rid3 or x = a3 by ENUMSET1:def 1;

        then not x in B2 by Lm5, Lm6, Lm7, Lm8, Lm9, Th15, ENUMSET1:def 1, FINSEQ_2: 53;

        hence x in (B1 \ B2) by A6, XBOOLE_0:def 5;

      end;

      then

       A7: B1 c= (B1 \ B2) by TARSKI:def 3;

      for x be object st x in (B1 \ B2) holds x in B1 by XBOOLE_0:def 5;

      then (B1 \ B2) c= B1 by TARSKI:def 3;

      then (B1 \ B2) = B1 by A7, XBOOLE_0:def 10;

      then

       A8: B1 misses B2 by XBOOLE_1: 83;

      set F = the addF of K;

      id3 in ( Permutations 3) by MATRIX_1:def 12;

      then

      reconsider r1 = (r . id3), r2 = (r . rid3), r3 = (r . a3), r4 = (r . a4), r5 = (r . a5), r6 = (r . a6) as Element of K by FUNCT_2: 5;

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

      then ( In (( Permutations 3),( Fin ( Permutations 3)))) = ( Permutations 3) by SUBSET_1:def 8;

      then

      reconsider X = {Id3, rid3, a3, a4, a5, a6} as Element of ( Fin ( Permutations 3)) by Th15, Th19, FINSEQ_2: 53;

      

       A9: (F $$ (B1,r)) = ((r1 + r2) + r3) & (F $$ (B2,r)) = ((r4 + r5) + r6) by Lm3, Lm4, Lm10, Lm11, Th15, FINSEQ_2: 53, SETWOP_2: 3;

      

       A10: (r . rid3) = (the multF of K $$ ( Path_matrix (rid3,M))) by Def1

      .= (the multF of K $$ <*c, e, g*>) by A1, Th15, Th21

      .= ((c * e) * g) by Th26;

      

       A11: (r . a3) = (the multF of K $$ ( Path_matrix (a3,M))) by Def1

      .= (the multF of K $$ <*a, f, h*>) by A1, Th22

      .= ((a * f) * h) by Th26;

      ( In (( Permutations 3),( Fin ( Permutations 3)))) = X & X = ( {Id3, rid3, a3} \/ {a4, a5, a6}) by Th15, Th19, ENUMSET1: 13, FINSEQ_2: 53;

      

      then ( Per M) = (F . ((F $$ (B1,r)),(F $$ (B2,r)))) by A8, SETWOP_2: 4

      .= (((r1 + r2) + r3) + (r4 + (r5 + r6))) by A9, RLVECT_1:def 3

      .= ((((r1 + r2) + r3) + r4) + (r5 + r6)) by RLVECT_1:def 3

      .= (((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h)) by A2, A10, A11, A5, A4, A3, RLVECT_1:def 3;

      hence thesis;

    end;

    theorem :: MATRIX_9:48

    

     Th48: for i,n be Element of NAT holds for p be Element of ( Permutations n) st i in ( Seg n) holds ex k be Element of NAT st k in ( Seg n) & i = (p . k)

    proof

      let i,n be Element of NAT ;

      let p be Element of ( Permutations n);

      

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

      then

       A2: ( dom p) = ( Seg n) by FUNCT_2: 52;

      then

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

      assume i in ( Seg n);

      then i in ( rng s) by A1, FUNCT_2:def 3;

      then ex k be Nat st k in ( dom s) & i = (s . k) by FINSEQ_2: 10;

      hence thesis by A2;

    end;

    theorem :: MATRIX_9:49

    

     Th49: for M be Matrix of n, K st (ex i be Element of NAT st i in ( Seg n) & for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K)) holds for p be Element of ( Permutations n) holds ex l be Element of NAT st l in ( Seg n) & (( Path_matrix (p,M)) . l) = ( 0. K)

    proof

      let M be Matrix of n, K;

      assume ex i be Element of NAT st i in ( Seg n) & for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K);

      then

      consider i be Element of NAT such that

       A1: i in ( Seg n) and

       A2: for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K);

      let p be Element of ( Permutations n);

      n in NAT by ORDINAL1:def 12;

      then

      consider k be Element of NAT such that

       A3: k in ( Seg n) and

       A4: i = (p . k) by A1, Th48;

      

       A5: 1 <= k by A3, FINSEQ_1: 1;

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

      then k <= ( len M) by A3, FINSEQ_1: 1;

      then

       A6: k in ( dom M) by A5, FINSEQ_3: 25;

      take k;

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

      then ( dom ( Path_matrix (p,M))) = ( Seg n) by FINSEQ_1:def 3;

      then (( Path_matrix (p,M)) . k) = (M * (k,i)) by A3, A4, MATRIX_3:def 7;

      then (( Path_matrix (p,M)) . k) = (( Col (M,i)) . k) by A6, MATRIX_0:def 8;

      hence thesis by A2, A3;

    end;

    theorem :: MATRIX_9:50

    

     Th50: for p be Element of ( Permutations n) holds for M be Matrix of n, K st (ex i be Element of NAT st i in ( Seg n) & for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K)) holds (( Path_product M) . p) = ( 0. K)

    proof

      let p be Element of ( Permutations n);

      let M be Matrix of n, K;

      

       A1: (( Path_product M) . p) = ( - ((the multF of K $$ ( Path_matrix (p,M))),p)) by MATRIX_3:def 8

      .= ( - (( Product ( Path_matrix (p,M))),p)) by GROUP_4:def 2;

      assume ex i be Element of NAT st i in ( Seg n) & for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K);

      then

      consider l be Element of NAT such that

       A2: l in ( Seg n) and

       A3: (( Path_matrix (p,M)) . l) = ( 0. K) by Th49;

      set k = l;

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

      then k in ( dom ( Path_matrix (p,M))) by A2, FINSEQ_1:def 3;

      then

       A4: ( Product ( Path_matrix (p,M))) = ( 0. K) by A3, FVSUM_1: 82;

      per cases ;

        suppose p is even;

        hence thesis by A4, A1, MATRIX_1:def 16;

      end;

        suppose p is odd;

        

        then ( - (( Product ( Path_matrix (p,M))),p)) = ( - ( Product ( Path_matrix (p,M)))) by MATRIX_1:def 16

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

        hence thesis by A1;

      end;

    end;

    theorem :: MATRIX_9:51

    

     Th51: for M be Matrix of n, K st (ex i be Element of NAT st i in ( Seg n) & for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K)) holds (the addF of K $$ (( In (( Permutations n),( Fin ( Permutations n)))),( Path_product M))) = ( 0. K)

    proof

      let M be Matrix of n, K;

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

      reconsider M1 = M as Matrix of n1, K;

      given i be Element of NAT such that

       A1: i in ( Seg n) & for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K);

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

      set f = ( Path_product M1);

      set F = the addF of K;

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

      then P1 = ( Permutations n) by SUBSET_1:def 8;

      then

      reconsider P1 as non empty Element of ( Fin ( Permutations n1));

      defpred P[ non empty Element of ( Fin ( Permutations n1))] means (F $$ ($1,f)) = ( 0. K);

      

       A2: for x be Element of ( Permutations n1), B be non empty Element of ( Fin ( Permutations n1)) st x in P1 & B c= P1 & not x in B & P[B] holds P[(B \/ {.x.})]

      proof

        let x be Element of ( Permutations n1), B be non empty Element of ( Fin ( Permutations n1));

        assume that x in P1 and B c= P1 and

         A3: not x in B and

         A4: P[B];

        (F $$ ((B \/ {.x.}),f)) = (F . ((F $$ (B,f)),(f . x))) by A3, SETWOP_2: 2

        .= ((F $$ (B,f)) + ( 0. K)) by A1, Th50

        .= ( 0. K) by A4, RLVECT_1: 4;

        hence thesis;

      end;

      

       A5: for x be Element of ( Permutations n1) st x in P1 holds P[ {.x.}]

      proof

        let x be Element of ( Permutations n1);

        assume x in P1;

        (F $$ ( {.x.},f)) = (f . x) by SETWISEO: 17

        .= ( 0. K) by A1, Th50;

        hence thesis;

      end;

       P[P1] from NonEmptyFiniteX( A5, A2);

      hence thesis;

    end;

    theorem :: MATRIX_9:52

    

     Th52: for p be Element of ( Permutations n) holds for M be Matrix of n, K st (ex i be Element of NAT st i in ( Seg n) & (for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K))) holds (( PPath_product M) . p) = ( 0. K)

    proof

      let p be Element of ( Permutations n);

      let M be Matrix of n, K;

      assume ex i be Element of NAT st i in ( Seg n) & for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K);

      then

      consider l be Element of NAT such that

       A1: l in ( Seg n) and

       A2: (( Path_matrix (p,M)) . l) = ( 0. K) by Th49;

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

      then l in ( dom ( Path_matrix (p,M))) by A1, FINSEQ_1:def 3;

      then

       A3: ( Product ( Path_matrix (p,M))) = ( 0. K) by A2, FVSUM_1: 82;

      (( PPath_product M) . p) = (the multF of K $$ ( Path_matrix (p,M))) by Def1

      .= ( 0. K) by A3, GROUP_4:def 2;

      hence thesis;

    end;

    

     Lm18: for M be Matrix of n, K st (ex i be Element of NAT st i in ( Seg n) & for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K)) holds (the addF of K $$ (( In (( Permutations n),( Fin ( Permutations n)))),( PPath_product M))) = ( 0. K)

    proof

      let M be Matrix of n, K;

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

      reconsider M1 = M as Matrix of n1, K;

      set F = the addF of K;

      set f = ( PPath_product M1);

      set P1 = ( In (( Permutations n1),( Fin ( Permutations n1))));

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

      then

      reconsider P1 as non empty Element of ( Fin ( Permutations n1)) by SUBSET_1:def 8;

      defpred P[ non empty Element of ( Fin ( Permutations n1))] means (F $$ ($1,f)) = ( 0. K);

      assume

       A1: ex i be Element of NAT st i in ( Seg n) & for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K);

      

       A2: for x be Element of ( Permutations n1), B be non empty Element of ( Fin ( Permutations n1)) st x in P1 & B c= P1 & not x in B & P[B] holds P[(B \/ {.x.})]

      proof

        let x be Element of ( Permutations n1), B be non empty Element of ( Fin ( Permutations n1));

        assume that x in P1 and B c= P1 and

         A3: not x in B and

         A4: P[B];

        (F $$ ((B \/ {.x.}),f)) = (F . ((F $$ (B,f)),(f . x))) by A3, SETWOP_2: 2

        .= ((F $$ (B,f)) + ( 0. K)) by A1, Th52

        .= ( 0. K) by A4, RLVECT_1: 4;

        hence thesis;

      end;

      

       A5: for x be Element of ( Permutations n1) st x in P1 holds P[ {.x.}]

      proof

        let x be Element of ( Permutations n1);

        assume x in P1;

        (F $$ ( {.x.},f)) = (f . x) by SETWISEO: 17

        .= ( 0. K) by A1, Th52;

        hence thesis;

      end;

       P[P1] from NonEmptyFiniteX( A5, A2);

      hence thesis;

    end;

    theorem :: MATRIX_9:53

    for M be Matrix of n, K st (ex i be Element of NAT st i in ( Seg n) & for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K)) holds ( Det M) = ( 0. K)

    proof

      let M be Matrix of n, K;

      assume

       A1: ex i be Element of NAT st i in ( Seg n) & for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K);

      set f = ( Path_product M);

      set F = the addF of K;

      ( Det M) = (F $$ (( In (( Permutations n),( Fin ( Permutations n)))),f)) by MATRIX_3:def 9

      .= ( 0. K) by A1, Th51;

      hence thesis;

    end;

    theorem :: MATRIX_9:54

    for M be Matrix of n, K st (ex i be Element of NAT st i in ( Seg n) & for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = ( 0. K)) holds ( Per M) = ( 0. K) by Lm18;

    begin

    theorem :: MATRIX_9:55

    for M,N be Matrix of n, K st i in ( Seg n) holds for p be Element of ( Permutations n) holds ex k be Element of NAT st k in ( Seg n) & i = (p . k) & (( Col (N,i)) /. k) = (( Path_matrix (p,N)) /. k)

    proof

      let M,N be Matrix of n, K;

      assume

       A1: i in ( Seg n);

      let p be Element of ( Permutations n);

      n in NAT by ORDINAL1:def 12;

      then

      consider k be Element of NAT such that

       A2: k in ( Seg n) and

       A3: i = (p . k) by A1, Th48;

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

      then

       A4: k in ( dom ( Path_matrix (p,N))) by A2, FINSEQ_1:def 3;

      then (( Path_matrix (p,N)) . k) = (N * (k,i)) by A3, MATRIX_3:def 7;

      then

       A5: (( Path_matrix (p,N)) /. k) = (N * (k,i)) by A4, PARTFUN1:def 6;

      take k;

      

       A6: ( len N) = n by MATRIX_0:def 2;

      then k in ( dom N) by A2, FINSEQ_1:def 3;

      then

       A7: (( Col (N,i)) . k) = (N * (k,i)) by MATRIX_0:def 8;

      ( len ( Col (N,i))) = ( len N) by MATRIX_0:def 8;

      then k in ( dom ( Col (N,i))) by A2, A6, FINSEQ_1:def 3;

      hence thesis by A2, A3, A5, A7, PARTFUN1:def 6;

    end;

    theorem :: MATRIX_9:56

    for a be Element of K holds for M,N be Matrix of n, K st (ex i be Element of NAT st i in ( Seg n) & (for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = (a * (( Col (N,i)) /. k))) & (for l be Element of NAT st l <> i & l in ( Seg n) holds ( Col (M,l)) = ( Col (N,l)))) holds for p be Element of ( Permutations n) holds ex l be Element of NAT st l in ( Seg n) & (( Path_matrix (p,M)) /. l) = (a * (( Path_matrix (p,N)) /. l))

    proof

      let a be Element of K;

      let M,N be Matrix of n, K;

      assume ex i be Element of NAT st i in ( Seg n) & (for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = (a * (( Col (N,i)) /. k))) & for l be Element of NAT st l <> i & l in ( Seg n) holds ( Col (M,l)) = ( Col (N,l));

      then

      consider i be Element of NAT such that

       A1: i in ( Seg n) and

       A2: for k be Element of NAT st k in ( Seg n) holds (( Col (M,i)) . k) = (a * (( Col (N,i)) /. k)) and for l be Element of NAT st l <> i & l in ( Seg n) holds ( Col (M,l)) = ( Col (N,l));

      let p be Element of ( Permutations n);

      n in NAT by ORDINAL1:def 12;

      then

      consider k be Element of NAT such that

       A3: k in ( Seg n) and

       A4: i = (p . k) by A1, Th48;

      

       A5: 1 <= k by A3, FINSEQ_1: 1;

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

      then

       A6: k in ( dom ( Path_matrix (p,N))) by A3, FINSEQ_1:def 3;

      then (( Path_matrix (p,N)) . k) = (N * (k,i)) by A4, MATRIX_3:def 7;

      then

       A7: (( Path_matrix (p,N)) /. k) = (N * (k,i)) by A6, PARTFUN1:def 6;

      ( len ( Col (N,i))) = ( len N) by MATRIX_0:def 8;

      then

       A8: ( dom ( Col (N,i))) = ( dom N) by FINSEQ_3: 29;

      ( len N) = n by MATRIX_0:def 2;

      then k <= ( len N) by A3, FINSEQ_1: 1;

      then

       A9: k in ( dom N) by A5, FINSEQ_3: 25;

      then (( Col (N,i)) . k) = (N * (k,i)) by MATRIX_0:def 8;

      then

       A10: (( Col (N,i)) /. k) = (( Path_matrix (p,N)) /. k) by A9, A7, A8, PARTFUN1:def 6;

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

      then k <= ( len M) by A3, FINSEQ_1: 1;

      then

       A11: k in ( dom M) by A5, FINSEQ_3: 25;

      take k;

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

      then

       A12: ( dom ( Path_matrix (p,M))) = ( Seg n) by FINSEQ_1:def 3;

      then (( Path_matrix (p,M)) . k) = (M * (k,i)) by A3, A4, MATRIX_3:def 7;

      

      then (( Path_matrix (p,M)) . k) = (( Col (M,i)) . k) by A11, MATRIX_0:def 8

      .= (a * (( Path_matrix (p,N)) /. k)) by A2, A3, A10;

      hence thesis by A12, A3, PARTFUN1:def 6;

    end;