matrix_3.miz



    begin

    reserve x,y,z,x1,x2,y1,y2,z1,z2 for object,

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

D for non empty set,

K for Ring;

    definition

      let K be Ring;

      let n,m be Nat;

      :: MATRIX_3:def1

      func 0. (K,n,m) -> Matrix of n, m, K equals (n |-> (m |-> ( 0. K)));

      coherence by MATRIX_0: 10;

    end

    definition

      let K be Ring;

      let A be Matrix of K;

      :: MATRIX_3:def2

      func - A -> Matrix of K means

      : Def2: ( len it ) = ( len A) & ( width it ) = ( width A) & for i, j holds [i, j] in ( Indices A) implies (it * (i,j)) = ( - (A * (i,j)));

      existence

      proof

        set n = ( len A);

        deffunc F( Nat, Nat) = ( - (A * ($1,$2)));

        consider M be Matrix of ( len A), ( width A), K such that

         A1: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = F(i,j) from MATRIX_0:sch 1;

        reconsider A1 = A as Matrix of n, ( width A), K by MATRIX_0: 51;

        

         A2: ( Indices A1) = [:( Seg n), ( Seg ( width A)):] by MATRIX_0: 25;

         A3:

        now

          per cases ;

            case n > 0 ;

            hence ( len M) = ( len A) & ( width M) = ( width A) & ( Indices A) = ( Indices M) by A2, MATRIX_0: 23;

          end;

            case

             A4: n = 0 ;

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

            then

             A5: ( width M) = 0 by MATRIX_0:def 3;

            ( width A) = 0 by A4, MATRIX_0:def 3;

            hence ( len M) = ( len A) & ( width M) = ( width A) & ( Indices A) = ( Indices M) by A2, A5, MATRIX_0: 25;

          end;

        end;

        reconsider M as Matrix of K;

        take M;

        thus thesis by A1, A3;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of K;

        set n = ( len A);

        assume that

         A6: ( len M1) = ( len A) & ( width M1) = ( width A) and

         A7: for i, j st [i, j] in ( Indices A) holds (M1 * (i,j)) = ( - (A * (i,j))) and

         A8: ( len M2) = ( len A) & ( width M2) = ( width A) and

         A9: for i, j st [i, j] in ( Indices A) holds (M2 * (i,j)) = ( - (A * (i,j)));

        reconsider M2 as Matrix of n, ( width A), K by A8, MATRIX_0: 51;

        reconsider M1 as Matrix of n, ( width A), K by A6, MATRIX_0: 51;

        reconsider A1 = A as Matrix of n, ( width A), K by MATRIX_0: 51;

        

         A10: ( Indices A1) = [:( Seg n), ( Seg ( width A)):] by MATRIX_0: 25;

        

         A11: ( Indices M1) = [:( Seg n), ( Seg ( width M1)):] & ( Indices M2) = [:( Seg n), ( Seg ( width M2)):] by MATRIX_0: 25;

         A12:

        now

          per cases ;

            case

             A13: n > 0 ;

            then ( Indices M1) = [:( Seg n), ( Seg ( width A)):] by MATRIX_0: 23;

            hence ( Indices A) = ( Indices M1) & ( Indices M1) = ( Indices M2) by A10, A13, MATRIX_0: 23;

          end;

            case

             A14: n = 0 ;

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

            then

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

            ( len M2) = 0 by A14, MATRIX_0:def 2;

            hence ( Indices A) = ( Indices M1) & ( Indices M1) = ( Indices M2) by A10, A11, A14, A15, MATRIX_0:def 3;

          end;

        end;

        now

          let i, j;

          assume

           A16: [i, j] in ( Indices A);

          then (M1 * (i,j)) = ( - (A * (i,j))) by A7;

          hence (M1 * (i,j)) = (M2 * (i,j)) by A9, A16;

        end;

        hence thesis by A12, MATRIX_0: 27;

      end;

    end

    definition

      let K be Ring;

      let A,B be Matrix of K;

      :: MATRIX_3:def3

      func A + B -> Matrix of K means

      : Def3: ( len it ) = ( len A) & ( width it ) = ( width A) & for i, j holds [i, j] in ( Indices A) implies (it * (i,j)) = ((A * (i,j)) + (B * (i,j)));

      existence

      proof

        set n = ( len A);

        reconsider A1 = A as Matrix of ( len A), ( width A), K by MATRIX_0: 51;

        deffunc F( Nat, Nat) = ((A * ($1,$2)) + (B * ($1,$2)));

        consider M be Matrix of ( len A), ( width A), K such that

         A1: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = F(i,j) from MATRIX_0:sch 1;

        

         A2: ( Indices A1) = [:( Seg ( len A)), ( Seg ( width A)):] by MATRIX_0: 25;

         A3:

        now

          per cases ;

            case n > 0 ;

            hence ( len M) = ( len A) & ( width M) = ( width A) & ( Indices A) = ( Indices M) by A2, MATRIX_0: 23;

          end;

            case

             A4: n = 0 ;

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

            then

             A5: ( width M) = 0 by MATRIX_0:def 3;

            ( width A) = 0 by A4, MATRIX_0:def 3;

            hence ( len M) = ( len A) & ( width M) = ( width A) & ( Indices A) = ( Indices M) by A2, A5, MATRIX_0: 25;

          end;

        end;

        reconsider M as Matrix of K;

        take M;

        thus thesis by A1, A3;

      end;

      uniqueness

      proof

        set n = ( len A);

        let M1,M2 be Matrix of K;

        assume that

         A6: ( len M1) = ( len A) & ( width M1) = ( width A) and

         A7: for i, j st [i, j] in ( Indices A) holds (M1 * (i,j)) = ((A * (i,j)) + (B * (i,j))) and

         A8: ( len M2) = ( len A) & ( width M2) = ( width A) and

         A9: for i, j st [i, j] in ( Indices A) holds (M2 * (i,j)) = ((A * (i,j)) + (B * (i,j)));

        reconsider M2 as Matrix of n, ( width A), K by A8, MATRIX_0: 51;

        reconsider M1 as Matrix of n, ( width A), K by A6, MATRIX_0: 51;

        reconsider A1 = A as Matrix of n, ( width A), K by MATRIX_0: 51;

        

         A10: ( Indices A1) = [:( Seg n), ( Seg ( width A)):] by MATRIX_0: 25;

        

         A11: ( Indices M1) = [:( Seg n), ( Seg ( width M1)):] & ( Indices M2) = [:( Seg n), ( Seg ( width M2)):] by MATRIX_0: 25;

         A12:

        now

          per cases ;

            case

             A13: n > 0 ;

            then ( Indices M1) = [:( Seg n), ( Seg ( width A)):] by MATRIX_0: 23;

            hence ( Indices A) = ( Indices M1) & ( Indices M1) = ( Indices M2) by A10, A13, MATRIX_0: 23;

          end;

            case

             A14: n = 0 ;

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

            then

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

            ( len M2) = 0 by A14, MATRIX_0:def 2;

            hence ( Indices A) = ( Indices M1) & ( Indices M1) = ( Indices M2) by A10, A11, A14, A15, MATRIX_0:def 3;

          end;

        end;

        now

          let i, j;

          assume

           A16: [i, j] in ( Indices A);

          then (M1 * (i,j)) = ((A * (i,j)) + (B * (i,j))) by A7;

          hence (M1 * (i,j)) = (M2 * (i,j)) by A9, A16;

        end;

        hence thesis by A12, MATRIX_0: 27;

      end;

    end

    theorem :: MATRIX_3:1

    

     Th1: for i, j st [i, j] in ( Indices ( 0. (K,n,m))) holds (( 0. (K,n,m)) * (i,j)) = ( 0. K)

    proof

      let i, j;

      assume

       A1: [i, j] in ( Indices ( 0. (K,n,m)));

      

       A2: ( Indices ( 0. (K,n,m))) = [:( Seg n), ( Seg ( width ( 0. (K,n,m)))):] by MATRIX_0: 25;

      per cases ;

        suppose

         A3: n > 0 ;

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

        

         A4: [i, j] in [:( Seg n), ( Seg m):] by A1, A3, MATRIX_0: 23;

        then j in ( Seg m) by ZFMISC_1: 87;

        then

         A5: ((m1 |-> ( 0. K)) . j) = ( 0. K) by FUNCOP_1: 7;

        i in ( Seg n) by A4, ZFMISC_1: 87;

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

        hence thesis by A1, A5, MATRIX_0:def 5;

      end;

        suppose n = 0 ;

        then ( Seg n) = {} ;

        hence thesis by A1, A2, ZFMISC_1: 90;

      end;

    end;

    theorem :: MATRIX_3:2

    for A,B be Matrix of K st ( len A) = ( len B) & ( width A) = ( width B) holds (A + B) = (B + A)

    proof

      let A,B be Matrix of K;

      assume that

       A1: ( len A) = ( len B) and

       A2: ( width A) = ( width B);

      

       A3: ( width A) = ( width (A + B)) by Def3;

      then

       A4: ( width (A + B)) = ( width (B + A)) by A2, Def3;

      

       A5: ( len A) = ( len (A + B)) by Def3;

      then ( dom A) = ( dom (A + B)) by FINSEQ_3: 29;

      then

       A6: ( Indices A) = ( Indices (A + B)) by A3;

      ( dom A) = ( dom B) by A1, FINSEQ_3: 29;

      then

       A7: ( Indices B) = [:( dom A), ( Seg ( width A)):] by A2;

       A8:

      now

        let i, j;

        assume

         A9: [i, j] in ( Indices (A + B));

        

        hence ((A + B) * (i,j)) = ((B * (i,j)) + (A * (i,j))) by A6, Def3

        .= ((B + A) * (i,j)) by A7, A6, A9, Def3;

      end;

      ( len (A + B)) = ( len (B + A)) by A1, A5, Def3;

      hence thesis by A4, A8, MATRIX_0: 21;

    end;

    theorem :: MATRIX_3:3

    for A,B,C be Matrix of K st ( len A) = ( len B) & ( width A) = ( width B) holds ((A + B) + C) = (A + (B + C))

    proof

      let A,B,C be Matrix of K;

      assume that

       A1: ( len A) = ( len B) and

       A2: ( width A) = ( width B);

      ( dom A) = ( dom B) by A1, FINSEQ_3: 29;

      then

       A3: ( Indices B) = [:( dom A), ( Seg ( width A)):] by A2;

      

       A4: ( Indices A) = [:( dom A), ( Seg ( width A)):];

      

       A5: ( width ((A + B) + C)) = ( width (A + B)) by Def3;

      

       A6: ( width (A + B)) = ( width A) by Def3;

      

       A7: ( len (A + (B + C))) = ( len A) & ( width (A + (B + C))) = ( width A) by Def3;

      

       A8: ( len (A + B)) = ( len A) by Def3;

      

       A9: ( len ((A + B) + C)) = ( len (A + B)) by Def3;

      then ( dom A) = ( dom ((A + B) + C)) by A8, FINSEQ_3: 29;

      then

       A10: ( Indices ((A + B) + C)) = [:( dom A), ( Seg ( width A)):] by A6, A5;

      ( dom A) = ( dom (A + B)) by A8, FINSEQ_3: 29;

      then

       A11: ( Indices (A + B)) = [:( dom A), ( Seg ( width A)):] by A6;

      now

        let i, j;

        assume

         A12: [i, j] in ( Indices ((A + B) + C));

        

        hence (((A + B) + C) * (i,j)) = (((A + B) * (i,j)) + (C * (i,j))) by A11, A10, Def3

        .= (((A * (i,j)) + (B * (i,j))) + (C * (i,j))) by A4, A10, A12, Def3

        .= ((A * (i,j)) + ((B * (i,j)) + (C * (i,j)))) by RLVECT_1:def 3

        .= ((A * (i,j)) + ((B + C) * (i,j))) by A3, A10, A12, Def3

        .= ((A + (B + C)) * (i,j)) by A4, A10, A12, Def3;

      end;

      hence thesis by A8, A6, A9, A5, A7, MATRIX_0: 21;

    end;

    theorem :: MATRIX_3:4

    for A be Matrix of n, m, K holds (A + ( 0. (K,n,m))) = A

    proof

      let A be Matrix of n, m, K;

      per cases ;

        suppose

         A1: n > 0 ;

        

         A2: ( width A) = ( width (A + ( 0. (K,n,m)))) by Def3;

        

         A3: ( Indices A) = [:( Seg n), ( Seg m):] by A1, MATRIX_0: 23;

        

         A4: ( len A) = ( len (A + ( 0. (K,n,m)))) by Def3;

        then ( dom A) = ( dom (A + ( 0. (K,n,m)))) by FINSEQ_3: 29;

        then

         A5: ( Indices A) = ( Indices (A + ( 0. (K,n,m)))) by A2;

        

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

        now

          let i, j;

          assume

           A7: [i, j] in ( Indices (A + ( 0. (K,n,m))));

          

          hence ((A + ( 0. (K,n,m))) * (i,j)) = ((A * (i,j)) + (( 0. (K,n,m)) * (i,j))) by A5, Def3

          .= ((A * (i,j)) + ( 0. K)) by A3, A6, A5, A7, Th1

          .= (A * (i,j)) by RLVECT_1: 4;

        end;

        hence thesis by A4, A2, MATRIX_0: 21;

      end;

        suppose

         A8: n = 0 ;

        

         A9: ( width A) = ( width (A + ( 0. (K,n,m)))) by Def3;

        

         A10: ( len A) = ( len (A + ( 0. (K,n,m)))) by Def3;

        then ( dom A) = ( dom (A + ( 0. (K,n,m)))) by FINSEQ_3: 29;

        then ( Indices A) = [:( dom A), ( Seg ( width A)):] & ( Indices (A + ( 0. (K,n,m)))) = [:( dom A), ( Seg ( width A)):] by A9;

        then for i, j st [i, j] in ( Indices (A + ( 0. (K,n,m)))) holds ((A + ( 0. (K,n,m))) * (i,j)) = (A * (i,j)) by A8, MATRIX_0: 22;

        hence thesis by A10, A9, MATRIX_0: 21;

      end;

    end;

    theorem :: MATRIX_3:5

    for A be Matrix of n, m, K holds (A + ( - A)) = ( 0. (K,n,m))

    proof

      let A be Matrix of n, m, K;

      

       A1: ( width ( - A)) = ( width A) by Def2;

      

       A2: ( len (A + ( - A))) = ( len A) by Def3;

      

       A3: ( width (A + ( - A))) = ( width A) by Def3;

      

       A4: ( len ( - A)) = ( len A) by Def2;

       A5:

      now

        per cases ;

          case

           A6: n > 0 ;

          then ( len (A + ( - A))) = n & ( width (A + ( - A))) = m by A2, A3, MATRIX_0: 23;

          hence ( len ( 0. (K,n,m))) = ( len (A + ( - A))) & ( width ( 0. (K,n,m))) = ( width (A + ( - A))) by A6, MATRIX_0: 23;

          ( dom A) = ( dom ( - A)) & ( dom A) = ( dom (A + ( - A))) by A4, A2, FINSEQ_3: 29;

          hence ( Indices A) = ( Indices ( - A)) & ( Indices A) = ( Indices (A + ( - A))) by A1, A3;

        end;

          case

           A7: n = 0 ;

          then

           A8: ( width A) = 0 by MATRIX_0: 22;

          then

           A9: ( Seg ( width ( - A))) = ( Seg 0 ) by A1;

          

           A10: ( len A) = 0 by A7, MATRIX_0: 22;

          then

           A11: ( dom ( - A)) = ( Seg 0 ) by A4, FINSEQ_1:def 3;

          

           A12: ( Indices ( - A)) = [:( dom ( - A)), ( Seg ( width ( - A))):]

          .= [:( Seg 0 ), ( Seg ( width ( - A))):] by A11

          .= [:( Seg 0 ), ( Seg 0 ) qua set:] by A9;

          ( dom (A + ( - A))) = ( Seg 0 ) by A2, A10, FINSEQ_1:def 3;

          then

           A13: ( Indices (A + ( - A))) = [:( Seg 0 ), ( Seg 0 ) qua set:] by A3, A8;

          ( len ( 0. (K,n,m))) = 0 & ( width ( 0. (K,n,m))) = 0 by A7, MATRIX_0: 22;

          hence ( len ( 0. (K,n,m))) = ( len (A + ( - A))) & ( width ( 0. (K,n,m))) = ( width (A + ( - A))) by A10, A8, Def3;

          ( Indices A) = {} by A7, MATRIX_0: 22;

          hence ( Indices A) = ( Indices ( - A)) & ( Indices A) = ( Indices (A + ( - A))) by A12, A13, ZFMISC_1: 90;

        end;

      end;

      

       A14: ( Indices A) = ( Indices ( 0. (K,n,m))) by MATRIX_0: 26;

      now

        let i, j;

        assume

         A15: [i, j] in ( Indices A);

        

        hence ((A + ( - A)) * (i,j)) = ((A * (i,j)) + (( - A) * (i,j))) by Def3

        .= ((A * (i,j)) + ( - (A * (i,j)))) by A15, Def2

        .= ( 0. K) by RLVECT_1: 5

        .= (( 0. (K,n,m)) * (i,j)) by A14, A15, Th1;

      end;

      hence thesis by A5, MATRIX_0: 21;

    end;

    definition

      let K be Ring;

      let A,B be Matrix of K;

      assume

       A1: ( width A) = ( len B);

      :: MATRIX_3:def4

      func A * B -> Matrix of K means

      : Def4: ( len it ) = ( len A) & ( width it ) = ( width B) & for i, j st [i, j] in ( Indices it ) holds (it * (i,j)) = (( Line (A,i)) "*" ( Col (B,j)));

      existence

      proof

        deffunc F( Nat, Nat) = (( Line (A,$1)) "*" ( Col (B,$2)));

        consider M be Matrix of ( len A), ( width B), K such that

         A2: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = F(i,j) from MATRIX_0:sch 1;

        take M;

        now

          per cases ;

            case ( len A) > 0 ;

            hence ( len M) = ( len A) & ( width M) = ( width B) by MATRIX_0: 23;

          end;

            case

             A3: ( len A) = 0 ;

            then ( len B) = 0 by A1, MATRIX_0:def 3;

            then

             A4: ( width B) = 0 by MATRIX_0:def 3;

            ( len M) = 0 by A3, MATRIX_0: 25;

            hence ( len M) = ( len A) & ( width M) = ( width B) by A3, A4, MATRIX_0:def 3;

          end;

        end;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of K;

        assume that

         A5: ( len M1) = ( len A) and

         A6: ( width M1) = ( width B) and

         A7: for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (( Line (A,i)) "*" ( Col (B,j))) and

         A8: ( len M2) = ( len A) and

         A9: ( width M2) = ( width B) and

         A10: for i, j st [i, j] in ( Indices M2) holds (M2 * (i,j)) = (( Line (A,i)) "*" ( Col (B,j)));

        ( dom M2) = ( dom M1) by A5, A8, FINSEQ_3: 29;

        then

         A11: ( Indices M1) = [:( dom M1), ( Seg ( width M1)):] & ( Indices M2) = [:( dom M1), ( Seg ( width M1)):] by A6, A9;

        now

          let i, j;

          assume

           A12: [i, j] in ( Indices M1);

          then (M1 * (i,j)) = (( Line (A,i)) "*" ( Col (B,j))) by A7;

          hence (M1 * (i,j)) = (M2 * (i,j)) by A10, A11, A12;

        end;

        hence thesis by A5, A6, A8, A9, MATRIX_0: 21;

      end;

    end

    definition

      let n, k, m;

      let K be Ring;

      let A be Matrix of n, k, K;

      let B be Matrix of ( width A), m, K;

      :: original: *

      redefine

      func A * B -> Matrix of ( len A), ( width B), K ;

      coherence

      proof

        ( width A) = ( len B) by MATRIX_0: 25;

        then ( len (A * B)) = ( len A) & ( width (A * B)) = ( width B) by Def4;

        hence thesis by MATRIX_0: 51;

      end;

    end

    definition

      let K be Ring;

      let M be Matrix of K;

      let a be Element of K;

      :: MATRIX_3:def5

      func a * M -> Matrix of K means ( len it ) = ( len M) & ( width it ) = ( width M) & for i, j st [i, j] in ( Indices M) holds (it * (i,j)) = (a * (M * (i,j)));

      existence

      proof

        deffunc F( Nat, Nat) = (a * (M * ($1,$2)));

        consider N be Matrix of ( len M), ( width M), K such that

         A1: for i, j st [i, j] in ( Indices N) holds (N * (i,j)) = F(i,j) from MATRIX_0:sch 1;

        take N;

        

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

         A3:

        now

          per cases ;

            case

             A4: ( len M) = 0 ;

            then ( width N) = 0 by A2, MATRIX_0:def 3;

            hence ( width N) = ( width M) by A4, MATRIX_0:def 3;

          end;

            case ( len M) > 0 ;

            hence ( width N) = ( width M) by MATRIX_0: 23;

          end;

        end;

        ( dom M) = ( dom N) by A2, FINSEQ_3: 29;

        then ( Indices N) = [:( dom M), ( Seg ( width M)):] by A3;

        hence thesis by A1, A3, MATRIX_0:def 2;

      end;

      uniqueness

      proof

        let A,B be Matrix of K;

        assume that

         A5: ( len A) = ( len M) and

         A6: ( width A) = ( width M) and

         A7: for i, j st [i, j] in ( Indices M) holds (A * (i,j)) = (a * (M * (i,j))) and

         A8: ( len B) = ( len M) & ( width B) = ( width M) and

         A9: for i, j st [i, j] in ( Indices M) holds (B * (i,j)) = (a * (M * (i,j)));

        now

          let i, j;

          ( dom A) = ( dom M) by A5, FINSEQ_3: 29;

          then

           A10: ( Indices A) = [:( dom M), ( Seg ( width M)):] by A6;

          assume

           A11: [i, j] in ( Indices A);

          

          hence (A * (i,j)) = (a * (M * (i,j))) by A7, A10

          .= (B * (i,j)) by A9, A11, A10;

        end;

        hence thesis by A5, A6, A8, MATRIX_0: 21;

      end;

    end

    definition

      let K be Ring;

      let M be Matrix of K;

      let a be Element of K;

      :: MATRIX_3:def6

      func M * a -> Matrix of K equals (a * M);

      coherence ;

    end

    theorem :: MATRIX_3:6

    for p,q be FinSequence of K st ( len p) = ( len q) holds ( len ( mlt (p,q))) = ( len p) & ( len ( mlt (p,q))) = ( len q)

    proof

      let p,q be FinSequence of K;

      reconsider r = ( mlt (p,q)) as FinSequence of K;

      

       A1: r = (the multF of K .: (p,q)) by FVSUM_1:def 7;

      assume ( len p) = ( len q);

      hence thesis by A1, FINSEQ_2: 72;

    end;

    theorem :: MATRIX_3:7

    for i, l st [i, l] in ( Indices ( 1. (K,n))) & l = i holds (( Line (( 1. (K,n)),i)) . l) = ( 1. K)

    proof

      let i, l;

      assume that

       A1: [i, l] in ( Indices ( 1. (K,n))) and

       A2: l = i;

      l in ( Seg ( width ( 1. (K,n)))) by A1, ZFMISC_1: 87;

      

      hence (( Line (( 1. (K,n)),i)) . l) = (( 1. (K,n)) * (i,l)) by MATRIX_0:def 7

      .= ( 1. K) by A1, A2, MATRIX_1:def 3;

    end;

    theorem :: MATRIX_3:8

    for i, l st [i, l] in ( Indices ( 1. (K,n))) & l <> i holds (( Line (( 1. (K,n)),i)) . l) = ( 0. K)

    proof

      let i, l;

      assume that

       A1: [i, l] in ( Indices ( 1. (K,n))) and

       A2: l <> i;

      l in ( Seg ( width ( 1. (K,n)))) by A1, ZFMISC_1: 87;

      

      hence (( Line (( 1. (K,n)),i)) . l) = (( 1. (K,n)) * (i,l)) by MATRIX_0:def 7

      .= ( 0. K) by A1, A2, MATRIX_1:def 3;

    end;

    theorem :: MATRIX_3:9

    for l, j st [l, j] in ( Indices ( 1. (K,n))) & l = j holds (( Col (( 1. (K,n)),j)) . l) = ( 1. K)

    proof

      let l, j;

      assume that

       A1: [l, j] in ( Indices ( 1. (K,n))) and

       A2: l = j;

      l in ( dom ( 1. (K,n))) by A1, ZFMISC_1: 87;

      

      hence (( Col (( 1. (K,n)),j)) . l) = (( 1. (K,n)) * (l,j)) by MATRIX_0:def 8

      .= ( 1. K) by A1, A2, MATRIX_1:def 3;

    end;

    theorem :: MATRIX_3:10

    for l, j st [l, j] in ( Indices ( 1. (K,n))) & l <> j holds (( Col (( 1. (K,n)),j)) . l) = ( 0. K)

    proof

      let l, j;

      assume that

       A1: [l, j] in ( Indices ( 1. (K,n))) and

       A2: l <> j;

      l in ( dom ( 1. (K,n))) by A1, ZFMISC_1: 87;

      

      hence (( Col (( 1. (K,n)),j)) . l) = (( 1. (K,n)) * (l,j)) by MATRIX_0:def 8

      .= ( 0. K) by A1, A2, MATRIX_1:def 3;

    end;

    

     Lm1: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p be FinSequence of L st for i be Element of NAT st i in ( dom p) holds (p . i) = ( 0. L) holds ( Sum p) = ( 0. L)

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let p be FinSequence of L;

      assume

       A1: for k be Element of NAT st k in ( dom p) holds (p . k) = ( 0. L);

      defpred P[ FinSequence of L] means (for k be Element of NAT st k in ( dom $1) holds ($1 . k) = ( 0. L)) implies ( Sum $1) = ( 0. L);

      

       A2: for p be FinSequence of L, x be Element of L st P[p] holds P[(p ^ <*x*>)]

      proof

        let p be FinSequence of L;

        let x be Element of L;

        assume

         A3: (for k be Element of NAT st k in ( dom p) holds (p . k) = ( 0. L)) implies ( Sum p) = ( 0. L);

        

         A4: (( len p) + 1) in ( Seg (( len p) + 1)) by FINSEQ_1: 4;

        assume

         A5: for k be Element of NAT st k in ( dom (p ^ <*x*>)) holds ((p ^ <*x*>) . k) = ( 0. L);

        

         A6: for k be Element of NAT st k in ( dom p) holds (p . k) = ( 0. L)

        proof

          

           A7: ( dom p) c= ( dom (p ^ <*x*>)) by FINSEQ_1: 26;

          let k be Element of NAT such that

           A8: k in ( dom p);

          

          thus (p . k) = ((p ^ <*x*>) . k) by A8, FINSEQ_1:def 7

          .= ( 0. L) by A5, A8, A7;

        end;

        ( len (p ^ <*x*>)) = (( len p) + ( len <*x*>)) by FINSEQ_1: 22

        .= (( len p) + 1) by FINSEQ_1: 39;

        then

         A9: (( len p) + 1) in ( dom (p ^ <*x*>)) by A4, FINSEQ_1:def 3;

        

         A10: x = ((p ^ <*x*>) . (( len p) + 1)) by FINSEQ_1: 42;

        

        thus ( Sum (p ^ <*x*>)) = (( Sum p) + ( Sum <*x*>)) by RLVECT_1: 41

        .= (( Sum p) + x) by RLVECT_1: 44

        .= (( 0. L) + ( 0. L)) by A3, A5, A6, A9, A10

        .= ( 0. L) by RLVECT_1:def 4;

      end;

      

       A11: P[( <*> the carrier of L)] by RLVECT_1: 43;

      for p be FinSequence of L holds P[p] from FINSEQ_2:sch 2( A11, A2);

      hence thesis by A1;

    end;

    theorem :: MATRIX_3:11

    

     Th11: for n be Element of NAT holds for K be add-associative right_zeroed right_complementable non empty addLoopStr holds ( Sum (n |-> ( 0. K))) = ( 0. K)

    proof

      let n be Element of NAT ;

      let K be add-associative right_zeroed right_complementable non empty addLoopStr;

      set p = (n |-> ( 0. K));

      for i be Element of NAT st i in ( dom p) holds (p . i) = ( 0. K)

      proof

        let i be Element of NAT ;

        assume i in ( dom p);

        then i in ( Seg n) by FUNCOP_1: 13;

        hence thesis by FUNCOP_1: 7;

      end;

      hence thesis by Lm1;

    end;

    theorem :: MATRIX_3:12

    

     Th12: for K be add-associative right_zeroed right_complementable non empty addLoopStr holds for p be FinSequence of K holds for i st i in ( dom p) & for k st k in ( dom p) & k <> i holds (p . k) = ( 0. K) holds ( Sum p) = (p . i)

    proof

      let K be add-associative right_zeroed right_complementable non empty addLoopStr;

      let p be FinSequence of K;

      let i;

      assume that

       A1: i in ( dom p) and

       A2: for k st k in ( dom p) & k <> i holds (p . k) = ( 0. K);

      reconsider a = (p . i) as Element of K by A1, FINSEQ_2: 11;

      reconsider p1 = (p | ( Seg i)) as FinSequence of K by FINSEQ_1: 18;

      i <> 0 by A1, FINSEQ_3: 25;

      then i in ( Seg i) by FINSEQ_1: 3;

      then i in (( dom p) /\ ( Seg i)) by A1, XBOOLE_0:def 4;

      then

       A3: i in ( dom p1) by RELAT_1: 61;

      then p1 <> {} ;

      then ( len p1) <> 0 ;

      then

      consider p3 be FinSequence of K, x be Element of K such that

       A4: p1 = (p3 ^ <*x*>) by FINSEQ_2: 19;

      p1 is_a_prefix_of p by TREES_1:def 1;

      then

      consider p2 be FinSequence such that

       A5: p = (p1 ^ p2) by TREES_1: 1;

      reconsider p2 as FinSequence of K by A5, FINSEQ_1: 36;

      

       A6: ( dom p2) = ( Seg ( len p2)) by FINSEQ_1:def 3;

      

       A7: for k st k in ( Seg ( len p2)) holds (p2 . k) = ( 0. K)

      proof

        let k;

        

         A8: i <= ( len p1) & ( len p1) <= (( len p1) + k) by A3, FINSEQ_3: 25, NAT_1: 12;

        assume k in ( Seg ( len p2));

        then

         A9: k in ( dom p2) by FINSEQ_1:def 3;

        then 0 <> k by FINSEQ_3: 25;

        then

         A10: i <> (( len p1) + k) by A8, XCMPLX_1: 3, XXREAL_0: 1;

        

        thus (p2 . k) = (p . (( len p1) + k)) by A5, A9, FINSEQ_1:def 7

        .= ( 0. K) by A2, A5, A9, A10, FINSEQ_1: 28;

      end;

       A11:

      now

        let j be Nat;

        assume

         A12: j in ( dom p2);

        

        hence (p2 . j) = ( 0. K) by A7, A6

        .= ((( len p2) |-> ( 0. K)) . j) by A6, A12, FINSEQ_2: 57;

      end;

      

       A13: ( dom p3) = ( Seg ( len p3)) by FINSEQ_1:def 3;

      i <= ( len p) by A1, FINSEQ_3: 25;

      

      then

       A14: i = ( len p1) by FINSEQ_1: 17

      .= (( len p3) + ( len <*x*>)) by A4, FINSEQ_1: 22

      .= (( len p3) + 1) by FINSEQ_1: 39;

      

      then

       A15: x = (p1 . i) by A4, FINSEQ_1: 42

      .= a by A5, A3, FINSEQ_1:def 7;

      

       A16: for k st k in ( Seg ( len p3)) holds (p3 . k) = ( 0. K)

      proof

        let k;

        assume

         A17: k in ( Seg ( len p3));

        then k <= ( len p3) by FINSEQ_1: 1;

        then

         A18: i <> k by A14, NAT_1: 13;

        

         A19: k in ( dom p3) by A17, FINSEQ_1:def 3;

        then

         A20: k in ( dom p1) by A4, FINSEQ_2: 15;

        

        thus (p3 . k) = (p1 . k) by A4, A19, FINSEQ_1:def 7

        .= (p . k) by A5, A20, FINSEQ_1:def 7

        .= ( 0. K) by A2, A5, A18, A20, FINSEQ_2: 15;

      end;

       A21:

      now

        let j be Nat;

        assume

         A22: j in ( dom p3);

        

        hence (p3 . j) = ( 0. K) by A16, A13

        .= ((( len p3) |-> ( 0. K)) . j) by A13, A22, FINSEQ_2: 57;

      end;

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

      then

       A23: p3 = (( len p3) |-> ( 0. K)) by A21, FINSEQ_2: 9;

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

      then p2 = (( len p2) |-> ( 0. K)) by A11, FINSEQ_2: 9;

      

      then ( Sum p) = (( Sum (p3 ^ <*x*>)) + ( Sum (( len p2) |-> ( 0. K)))) by A5, A4, RLVECT_1: 41

      .= (( Sum (p3 ^ <*x*>)) + ( 0. K)) by Th11

      .= ( Sum (p3 ^ <*x*>)) by RLVECT_1: 4

      .= (( Sum (( len p3) |-> ( 0. K))) + x) by A23, FVSUM_1: 71

      .= (( 0. K) + a) by A15, Th11

      .= (p . i) by RLVECT_1: 4;

      hence thesis;

    end;

    theorem :: MATRIX_3:13

    

     Th13: for p,q be FinSequence of K holds ( len ( mlt (p,q))) = ( min (( len p),( len q)))

    proof

      let p,q be FinSequence of K;

      reconsider r = ( mlt (p,q)) as FinSequence of K;

      r = (the multF of K .: (p,q)) by FVSUM_1:def 7;

      hence thesis by FINSEQ_2: 71;

    end;

    theorem :: MATRIX_3:14

    

     Th14: for K be Ring holds for p,q be FinSequence of K holds for i st (p . i) = ( 1. K) & for k st k in ( dom p) & k <> i holds (p . k) = ( 0. K) holds for j st j in ( dom ( mlt (p,q))) holds (i = j implies (( mlt (p,q)) . j) = (q . i)) & (i <> j implies (( mlt (p,q)) . j) = ( 0. K))

    proof

      let K be Ring;

      let p,q be FinSequence of K;

      let i;

      assume that

       A1: (p . i) = ( 1. K) and

       A2: for k st k in ( dom p) & k <> i holds (p . k) = ( 0. K);

      let j;

      assume

       A3: j in ( dom ( mlt (p,q)));

      

       A4: ( dom p) = ( Seg ( len p)) & ( dom q) = ( Seg ( len q)) by FINSEQ_1:def 3;

      reconsider j1 = j as Element of NAT by ORDINAL1:def 12;

      ( dom ( mlt (p,q))) = ( Seg ( len ( mlt (p,q)))) & ( len ( mlt (p,q))) = ( min (( len p),( len q))) by Th13, FINSEQ_1:def 3;

      then

       A5: j in (( dom p) /\ ( dom q)) by A3, A4, FINSEQ_2: 2;

      then

       A6: j in ( dom q) by XBOOLE_0:def 4;

      then

      reconsider b = (q . j1) as Element of K by FINSEQ_2: 11;

      thus i = j implies (( mlt (p,q)) . j) = (q . i)

      proof

        reconsider b = (q . j1) as Element of K by A6, FINSEQ_2: 11;

        assume

         A7: i = j;

        

        hence (( mlt (p,q)) . j) = (( 1. K) * b) by A1, A3, FVSUM_1: 60

        .= (q . i) by A7;

      end;

      assume

       A8: i <> j;

      j in ( dom p) by A5, XBOOLE_0:def 4;

      then (p . j) = ( 0. K) by A2, A8;

      

      hence (( mlt (p,q)) . j) = (( 0. K) * b) by A3, FVSUM_1: 60

      .= ( 0. K);

    end;

    theorem :: MATRIX_3:15

    

     Th15: for i, j st [i, j] in ( Indices ( 1. (K,n))) holds (i = j implies (( Line (( 1. (K,n)),i)) . j) = ( 1. K)) & (i <> j implies (( Line (( 1. (K,n)),i)) . j) = ( 0. K))

    proof

      let i, j;

      set B = ( 1. (K,n));

      assume

       A1: [i, j] in ( Indices ( 1. (K,n)));

      then j in ( Seg ( width B)) by ZFMISC_1: 87;

      then

       A2: (( Line (B,i)) . j) = (B * (i,j)) by MATRIX_0:def 7;

      hence i = j implies (( Line (( 1. (K,n)),i)) . j) = ( 1. K) by A1, MATRIX_1:def 3;

      thus thesis by A1, A2, MATRIX_1:def 3;

    end;

    theorem :: MATRIX_3:16

    

     Th16: for i, j st [i, j] in ( Indices ( 1. (K,n))) holds (i = j implies (( Col (( 1. (K,n)),j)) . i) = ( 1. K)) & (i <> j implies (( Col (( 1. (K,n)),j)) . i) = ( 0. K))

    proof

      let i, j;

      set B = ( 1. (K,n));

      assume

       A1: [i, j] in ( Indices ( 1. (K,n)));

      then i in ( dom B) by ZFMISC_1: 87;

      then

       A2: (( Col (B,j)) . i) = (B * (i,j)) by MATRIX_0:def 8;

      hence i = j implies (( Col (( 1. (K,n)),j)) . i) = ( 1. K) by A1, MATRIX_1:def 3;

      thus thesis by A1, A2, MATRIX_1:def 3;

    end;

    theorem :: MATRIX_3:17

    

     Th17: for K be Ring holds for p,q be FinSequence of K holds for i st i in ( dom p) & i in ( dom q) & (p . i) = ( 1. K) & for k st k in ( dom p) & k <> i holds (p . k) = ( 0. K) holds ( Sum ( mlt (p,q))) = (q . i)

    proof

      let K be Ring;

      let p,q be FinSequence of K;

      let i;

      assume that

       A1: i in ( dom p) & i in ( dom q) and

       A2: (p . i) = ( 1. K) & for k st k in ( dom p) & k <> i holds (p . k) = ( 0. K);

      reconsider r = ( mlt (p,q)) as FinSequence of K;

      

       A3: for k st k in ( dom r) & k <> i holds (r . k) = ( 0. K) by A2, Th14;

      

       A4: ( dom p) = ( Seg ( len p)) & ( dom q) = ( Seg ( len q)) by FINSEQ_1:def 3;

      ( dom ( mlt (p,q))) = ( Seg ( len ( mlt (p,q)))) & ( len ( mlt (p,q))) = ( min (( len p),( len q))) by Th13, FINSEQ_1:def 3;

      then (( dom p) /\ ( dom q)) = ( dom ( mlt (p,q))) by A4, FINSEQ_2: 2;

      then

       A5: i in ( dom r) by A1, XBOOLE_0:def 4;

      then (r . i) = (q . i) by A2, Th14;

      hence thesis by A5, A3, Th12;

    end;

    theorem :: MATRIX_3:18

    for K be Ring holds for A be Matrix of n, K holds (( 1. (K,n)) * A) = A

    proof

      let K be Ring;

      let A be Matrix of n, K;

      set B = ( 1. (K,n));

      

       A1: ( len B) = n by MATRIX_0: 24;

      

       A2: ( len A) = n by MATRIX_0: 24;

      

       A3: ( width B) = n by MATRIX_0: 24;

      then

       A4: ( len (B * A)) = ( len B) by A2, Def4;

       A5:

      now

        

         A6: ( dom A) = ( Seg ( len A)) by FINSEQ_1:def 3;

        let i, j;

        assume

         A7: [i, j] in ( Indices (B * A));

        

         A8: ( dom (B * A)) = ( Seg ( len (B * A))) & ( Indices (B * A)) = [:( dom (B * A)), ( Seg ( width (B * A))):] by FINSEQ_1:def 3;

        then

         A9: i in ( Seg ( width B)) by A1, A3, A4, A7, ZFMISC_1: 87;

        then i in ( Seg ( len ( Line (B,i)))) by MATRIX_0:def 7;

        then

         A10: i in ( dom ( Line (B,i))) by FINSEQ_1:def 3;

        

         A11: ( dom B) = ( Seg ( len B)) by FINSEQ_1:def 3;

        then

         A12: i in ( dom B) by A4, A7, A8, ZFMISC_1: 87;

        then [i, i] in [:( dom B), ( Seg ( width B)):] by A9, ZFMISC_1: 87;

        then [i, i] in ( Indices B);

        then

         A13: (( Line (B,i)) . i) = ( 1. K) by Th15;

         A14:

        now

          let k;

          assume that

           A15: k in ( dom ( Line (B,i))) and

           A16: k <> i;

          k in ( Seg ( len ( Line (B,i)))) by A15, FINSEQ_1:def 3;

          then k in ( Seg ( width B)) by MATRIX_0:def 7;

          then [i, k] in [:( dom B), ( Seg ( width B)):] by A12, ZFMISC_1: 87;

          then [i, k] in ( Indices B);

          hence (( Line (B,i)) . k) = ( 0. K) by A16, Th15;

        end;

        i in ( Seg ( len ( Col (A,j)))) by A3, A2, A9, MATRIX_0:def 8;

        then

         A17: i in ( dom ( Col (A,j))) by FINSEQ_1:def 3;

        

        thus ((B * A) * (i,j)) = (( Line (B,i)) "*" ( Col (A,j))) by A3, A2, A7, Def4

        .= ( Sum ( mlt (( Line (B,i)),( Col (A,j))))) by FVSUM_1:def 9

        .= (( Col (A,j)) . i) by A10, A17, A14, A13, Th17

        .= (A * (i,j)) by A1, A2, A6, A11, A12, MATRIX_0:def 8;

      end;

      ( width (B * A)) = ( width A) by A3, A2, Def4;

      hence thesis by A1, A2, A4, A5, MATRIX_0: 21;

    end;

    theorem :: MATRIX_3:19

    for K be commutative Ring holds for A be Matrix of n, K holds (A * ( 1. (K,n))) = A

    proof

      let K be commutative Ring;

      let A be Matrix of n, K;

      set B = ( 1. (K,n));

      

       A1: ( width B) = n by MATRIX_0: 24;

      

       A2: ( width A) = n by MATRIX_0: 24;

      

       A3: ( len B) = n by MATRIX_0: 24;

      then

       A4: ( width (A * B)) = ( width B) by A2, Def4;

       A5:

      now

        let i, j;

        assume

         A6: [i, j] in ( Indices (A * B));

        then

         A7: j in ( Seg ( width B)) by A4, ZFMISC_1: 87;

        then j in ( Seg ( len ( Col (B,j)))) by A3, A1, MATRIX_0:def 8;

        then

         A8: j in ( dom ( Col (B,j))) by FINSEQ_1:def 3;

        

         A9: j in ( Seg ( width A)) by A1, A2, A4, A6, ZFMISC_1: 87;

         A10:

        now

          let k;

          assume that

           A11: k in ( dom ( Col (B,j))) and

           A12: k <> j;

          k in ( Seg ( len ( Col (B,j)))) by A11, FINSEQ_1:def 3;

          then k in ( Seg ( len B)) by MATRIX_0:def 8;

          then k in ( dom B) by FINSEQ_1:def 3;

          then [k, j] in [:( dom B), ( Seg ( width B)):] by A7, ZFMISC_1: 87;

          then [k, j] in ( Indices B);

          hence (( Col (B,j)) . k) = ( 0. K) by A12, Th16;

        end;

        j in ( dom B) by A3, A1, A7, FINSEQ_1:def 3;

        then [j, j] in [:( dom B), ( Seg ( width B)):] by A1, A2, A9, ZFMISC_1: 87;

        then [j, j] in ( Indices B);

        then

         A13: (( Col (B,j)) . j) = ( 1. K) by Th16;

        j in ( Seg ( len ( Line (A,i)))) by A1, A2, A7, MATRIX_0:def 7;

        then

         A14: j in ( dom ( Line (A,i))) by FINSEQ_1:def 3;

        

        thus ((A * B) * (i,j)) = (( Line (A,i)) "*" ( Col (B,j))) by A3, A2, A6, Def4

        .= (( Col (B,j)) "*" ( Line (A,i))) by FVSUM_1: 90

        .= ( Sum ( mlt (( Col (B,j)),( Line (A,i))))) by FVSUM_1:def 9

        .= (( Line (A,i)) . j) by A8, A14, A10, A13, Th17

        .= (A * (i,j)) by A9, MATRIX_0:def 7;

      end;

      ( len (A * B)) = ( len A) by A3, A2, Def4;

      hence thesis by A1, A2, A4, A5, MATRIX_0: 21;

    end;

    theorem :: MATRIX_3:20

    for K be Field holds for a,b be Element of K holds ( <* <*a*>*> * <* <*b*>*>) = <* <*(a * b)*>*>

    proof

      let K be Field;

      let a,b be Element of K;

      reconsider A = <* <*a*>*> as Matrix of 1, K;

      reconsider B = <* <*b*>*> as Matrix of 1, K;

      reconsider C = (A * B) as Matrix of K;

      

       A1: ( len ( Line (A,1))) = ( width A) by MATRIX_0:def 7

      .= 1 by MATRIX_0: 24;

      

       A2: ( width A) = 1 by MATRIX_0: 24;

      then 1 in ( Seg ( width A)) by FINSEQ_1: 2, TARSKI:def 1;

      

      then (( Line (A,1)) . 1) = ( <* <*a*>*> * (1,1)) by MATRIX_0:def 7

      .= a by MATRIX_0: 49;

      then

       A3: ( Line ( <* <*a*>*>,1)) = <*a*> by A1, FINSEQ_1: 40;

      

       A4: ( len B) = 1 by MATRIX_0: 24;

      then 1 in ( Seg ( len B)) by FINSEQ_1: 2, TARSKI:def 1;

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

      

      then

       A5: (( Col (B,1)) . 1) = ( <* <*b*>*> * (1,1)) by MATRIX_0:def 8

      .= b by MATRIX_0: 49;

      ( len A) = 1 by MATRIX_0: 24;

      then

       A6: ( len C) = 1 by A2, A4, Def4;

      ( width B) = 1 by MATRIX_0: 24;

      then

       A7: ( width C) = 1 by A2, A4, Def4;

      then

      reconsider C as Matrix of 1, K by A6, MATRIX_0: 51;

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

      then

       A8: ( Indices C) = [:( Seg 1), ( Seg 1):] by A6, A7;

      ( len ( Col (B,1))) = ( len B) by MATRIX_0:def 8

      .= 1 by MATRIX_0: 24;

      then

       A9: ( Col ( <* <*b*>*>,1)) = <*b*> by A5, FINSEQ_1: 40;

      now

        let i, j;

        assume

         A10: [i, j] in ( Indices C);

        then j in ( Seg 1) by A8, ZFMISC_1: 87;

        then

         A11: j = 1 by FINSEQ_1: 2, TARSKI:def 1;

        i in ( Seg 1) by A8, A10, ZFMISC_1: 87;

        then

         A12: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

        

        hence (C * (i,j)) = ( <*a*> "*" <*b*>) by A2, A4, A3, A9, A10, A11, Def4

        .= (a * b) by FVSUM_1: 88

        .= ( <* <*(a * b)*>*> * (i,j)) by A12, A11, MATRIX_0: 49;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    theorem :: MATRIX_3:21

    for K be Field holds for a1,a2,b1,b2,c1,c2,d1,d2 be Element of K holds (((a1,b1) ][ (c1,d1)) * ((a2,b2) ][ (c2,d2))) = ((((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2))))

    proof

      let K be Field;

      let a1,a2,b1,b2,c1,c2,d1,d2 be Element of K;

      reconsider A = ((a1,b1) ][ (c1,d1)) as Matrix of 2, K;

      reconsider B = ((a2,b2) ][ (c2,d2)) as Matrix of 2, K;

      reconsider D = ((((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2)))) as Matrix of 2, K;

      

       A1: ( width A) = 2 by MATRIX_0: 24;

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

      

      then

       A2: (( Line (A,2)) . 2) = (A * (2,2)) by A1, FINSEQ_1: 2, MATRIX_0:def 7

      .= d1 by MATRIX_0: 50;

      

       A3: ( len ( Line (A,2))) = ( width A) by MATRIX_0:def 7

      .= 2 by MATRIX_0: 24;

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

      

      then (( Line (A,2)) . 1) = (A * (2,1)) by A1, FINSEQ_1: 2, MATRIX_0:def 7

      .= c1 by MATRIX_0: 50;

      then

       A4: ( Line (A,2)) = <*c1, d1*> by A3, A2, FINSEQ_1: 44;

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

      

      then

       A5: (( Line (A,1)) . 2) = (A * (1,2)) by A1, FINSEQ_1: 2, MATRIX_0:def 7

      .= b1 by MATRIX_0: 50;

      

       A6: ( len ( Line (A,1))) = ( width A) by MATRIX_0:def 7

      .= 2 by MATRIX_0: 24;

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

      

      then (( Line (A,1)) . 1) = (A * (1,1)) by A1, FINSEQ_1: 2, MATRIX_0:def 7

      .= a1 by MATRIX_0: 50;

      then

       A7: ( Line (A,1)) = <*a1, b1*> by A6, A5, FINSEQ_1: 44;

      

       A8: ( len ( Col (B,2))) = ( len B) by MATRIX_0:def 8

      .= 2 by MATRIX_0: 24;

      

       A9: ( len ( Col (B,1))) = ( len B) by MATRIX_0:def 8

      .= 2 by MATRIX_0: 24;

      reconsider C = (A * B) as Matrix of K;

      

       A10: ( len B) = 2 by MATRIX_0: 24;

      ( width B) = 2 by MATRIX_0: 24;

      then

       A11: ( width C) = 2 by A1, A10, Def4;

      ( len A) = 2 by MATRIX_0: 24;

      then

       A12: ( len C) = 2 by A1, A10, Def4;

      then

      reconsider C as Matrix of 2, K by A11, MATRIX_0: 51;

      

       A13: ( Seg ( len B)) = ( dom B) by FINSEQ_1:def 3;

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

      

      then

       A14: (( Col (B,2)) . 2) = (B * (2,2)) by A10, A13, FINSEQ_1: 2, MATRIX_0:def 8

      .= d2 by MATRIX_0: 50;

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

      

      then (( Col (B,2)) . 1) = (B * (1,2)) by A10, A13, FINSEQ_1: 2, MATRIX_0:def 8

      .= b2 by MATRIX_0: 50;

      then

       A15: ( Col (B,2)) = <*b2, d2*> by A8, A14, FINSEQ_1: 44;

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

      

      then

       A16: (( Col (B,1)) . 2) = (B * (2,1)) by A10, A13, FINSEQ_1: 2, MATRIX_0:def 8

      .= c2 by MATRIX_0: 50;

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

      

      then (( Col (B,1)) . 1) = (B * (1,1)) by A10, A13, FINSEQ_1: 2, MATRIX_0:def 8

      .= a2 by MATRIX_0: 50;

      then

       A17: ( Col (B,1)) = <*a2, c2*> by A9, A16, FINSEQ_1: 44;

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

      then

       A18: ( Indices C) = [:( Seg 2), ( Seg 2):] by A12, A11;

      now

        let i, j;

        assume

         A19: [i, j] in ( Indices C);

        then

         A20: i in ( Seg 2) & j in ( Seg 2) by A18, ZFMISC_1: 87;

        now

          per cases by A20, FINSEQ_1: 2, TARSKI:def 2;

            case i = 1 & j = 1;

            

            hence (C * (1,1)) = ( <*a1, b1*> "*" <*a2, c2*>) by A1, A10, A7, A17, A19, Def4

            .= ((a1 * a2) + (b1 * c2)) by FVSUM_1: 89

            .= (D * (1,1)) by MATRIX_0: 50;

          end;

            case i = 1 & j = 2;

            

            hence (C * (1,2)) = ( <*a1, b1*> "*" <*b2, d2*>) by A1, A10, A7, A15, A19, Def4

            .= ((a1 * b2) + (b1 * d2)) by FVSUM_1: 89

            .= (D * (1,2)) by MATRIX_0: 50;

          end;

            case i = 2 & j = 1;

            

            hence (C * (2,1)) = ( <*c1, d1*> "*" <*a2, c2*>) by A1, A10, A4, A17, A19, Def4

            .= ((c1 * a2) + (d1 * c2)) by FVSUM_1: 89

            .= (D * (2,1)) by MATRIX_0: 50;

          end;

            case i = 2 & j = 2;

            

            hence (C * (2,2)) = ( <*c1, d1*> "*" <*b2, d2*>) by A1, A10, A4, A15, A19, Def4

            .= ((c1 * b2) + (d1 * d2)) by FVSUM_1: 89

            .= (D * (2,2)) by MATRIX_0: 50;

          end;

        end;

        hence (C * (i,j)) = (D * (i,j));

      end;

      hence thesis by MATRIX_0: 27;

    end;

    theorem :: MATRIX_3:22

    for K be Field holds for A,B be Matrix of K st ( width A) = ( len B) & ( width B) <> 0 holds ((A * B) @ ) = ((B @ ) * (A @ ))

    proof

      let K be Field;

      let A,B be Matrix of K;

      assume that

       A1: ( width A) = ( len B) and

       A2: ( width B) <> 0 ;

      

       A3: ( len (B @ )) = ( width B) by MATRIX_0:def 6;

      ( len (A @ )) = ( width A) by MATRIX_0:def 6;

      then

       A4: ( width (B @ )) = ( len (A @ )) by A1, A2, MATRIX_0: 54;

      then

       A5: ( width ((B @ ) * (A @ ))) = ( width (A @ )) by Def4;

      ( width (A * B)) > 0 by A1, A2, Def4;

      

      then

       A6: ( width ((A * B) @ )) = ( len (A * B)) by MATRIX_0: 54

      .= ( len A) by A1, Def4;

      

       A7: ( width ((B @ ) * (A @ ))) = ( width (A @ )) by A4, Def4;

      

       A8: ( len ((B @ ) * (A @ ))) = ( len (B @ )) by A4, Def4

      .= ( width B) by MATRIX_0:def 6;

      

       A9: ( len ((B @ ) * (A @ ))) = ( len (B @ )) by A4, Def4;

       A10:

      now

        let i, j;

        assume

         A11: [i, j] in ( Indices ((B @ ) * (A @ )));

        ( dom ((B @ ) * (A @ ))) = ( dom (B @ )) by A9, FINSEQ_3: 29;

        then

         A12: [i, j] in [:( dom (B @ )), ( Seg ( width (A @ ))):] by A5, A11;

        per cases ;

          suppose ( width A) = 0 ;

          hence (((B @ ) * (A @ )) * (i,j)) = (((A * B) @ ) * (i,j)) by A1, A2, MATRIX_0:def 3;

        end;

          suppose ( width A) > 0 ;

          then ( width (A @ )) = ( len A) by MATRIX_0: 54;

          then ( Seg ( width (A @ ))) = ( dom A) by FINSEQ_1:def 3;

          then

           A13: j in ( dom A) by A12, ZFMISC_1: 87;

          then

           A14: ( Col ((A @ ),j)) = ( Line (A,j)) by MATRIX_0: 58;

          j in ( Seg ( len A)) by A13, FINSEQ_1:def 3;

          then j in ( Seg ( len (A * B))) by A1, Def4;

          then

           A15: j in ( dom (A * B)) by FINSEQ_1:def 3;

          ( Seg ( width B)) = ( dom (B @ )) by A3, FINSEQ_1:def 3;

          then

           A16: i in ( Seg ( width B)) by A12, ZFMISC_1: 87;

          then i in ( Seg ( width (A * B))) by A1, Def4;

          then [j, i] in [:( dom (A * B)), ( Seg ( width (A * B))):] by A15, ZFMISC_1: 87;

          then

           A17: [j, i] in ( Indices (A * B));

          ( Line ((B @ ),i)) = ( Col (B,i)) by A16, MATRIX_0: 59;

          

          hence (((B @ ) * (A @ )) * (i,j)) = (( Col (B,i)) "*" ( Line (A,j))) by A4, A11, A14, Def4

          .= (( Line (A,j)) "*" ( Col (B,i))) by FVSUM_1: 90

          .= ((A * B) * (j,i)) by A1, A17, Def4

          .= (((A * B) @ ) * (i,j)) by A17, MATRIX_0:def 6;

        end;

      end;

      

       A18: ( width (A @ )) = ( len A)

      proof

        per cases ;

          suppose ( width A) = 0 ;

          hence thesis by A1, A2, MATRIX_0:def 3;

        end;

          suppose ( width A) > 0 ;

          hence thesis by MATRIX_0: 54;

        end;

      end;

      ( len ((A * B) @ )) = ( width (A * B)) by MATRIX_0:def 6

      .= ( width B) by A1, Def4;

      hence thesis by A6, A8, A7, A10, A18, MATRIX_0: 21;

    end;

    begin

    definition

      let I,J be non empty set;

      let X be Element of ( Fin I);

      let Y be Element of ( Fin J);

      :: original: [:

      redefine

      func [:X,Y:] -> Element of ( Fin [:I, J:]) ;

      coherence

      proof

        X c= I & Y c= J by FINSUB_1:def 5;

        then [:X, Y:] c= [:I, J:] by ZFMISC_1: 96;

        hence thesis by FINSUB_1:def 5;

      end;

    end

    definition

      let I,J,D be non empty set;

      let G be BinOp of D;

      let f be Function of I, D;

      let g be Function of J, D;

      :: original: *

      redefine

      func G * (f,g) -> Function of [:I, J:], D ;

      coherence by FINSEQOP: 79;

    end

    theorem :: MATRIX_3:23

    

     Th23: for I,J,D be non empty set holds for F,G be BinOp of D holds for f be Function of I, D holds for g be Function of J, D holds for X be Element of ( Fin I) holds for Y be Element of ( Fin J) st F is commutative & F is associative & ( [:Y, X:] <> {} or F is having_a_unity) & G is commutative holds (F $$ ( [:X, Y:],(G * (f,g)))) = (F $$ ( [:Y, X:],(G * (g,f))))

    proof

      deffunc F( object, object) = [$2, $1];

      let I,J,D be non empty set;

      let F,G be BinOp of D;

      let f be Function of I, D;

      let g be Function of J, D;

      let X be Element of ( Fin I), Y be Element of ( Fin J);

      assume

       A1: F is commutative & F is associative & ( [:Y, X:] <> {} or F is having_a_unity);

      consider h be Function such that

       A2: ( dom h) = [:J, I:] & for x,y be object st x in J & y in I holds (h . (x,y)) = F(x,y) from FUNCT_3:sch 2;

      now

        let z1,z2 be object;

        assume that

         A3: z1 in ( dom h) and

         A4: z2 in ( dom h) and

         A5: (h . z1) = (h . z2);

        consider x2,y2 be object such that

         A6: z2 = [x2, y2] by A2, A4, RELAT_1:def 1;

        x2 in J & y2 in I by A2, A4, A6, ZFMISC_1: 87;

        then

         A7: (h . (x2,y2)) = [y2, x2] by A2;

        consider x1,y1 be object such that

         A8: z1 = [x1, y1] by A2, A3, RELAT_1:def 1;

        x1 in J & y1 in I by A2, A3, A8, ZFMISC_1: 87;

        then

         A9: (h . (x1,y1)) = [y1, x1] by A2;

        then y1 = y2 by A5, A8, A6, A7, XTUPLE_0: 1;

        hence z1 = z2 by A5, A8, A6, A9, A7, XTUPLE_0: 1;

      end;

      then

       A10: h is one-to-one by FUNCT_1:def 4;

      

       A11: for x st x in [:J, I:] holds (h . x) in [:I, J:]

      proof

        let x;

        assume

         A12: x in [:J, I:];

        then

        consider y,z be object such that

         A13: x = [y, z] by RELAT_1:def 1;

        

         A14: y in J & z in I by A12, A13, ZFMISC_1: 87;

        then (h . (y,z)) = [z, y] by A2;

        hence thesis by A13, A14, ZFMISC_1: 87;

      end;

      assume

       A15: G is commutative;

      

       A16: (G * (g,f)) = ((G * (f,g)) * h)

      proof

        reconsider G as Function of [:D, D:], D;

        

         A17: ( dom (G * (g,f))) = [:J, I:] by FUNCT_2:def 1;

        

         A18: ( dom (G * (f,g))) = [:I, J:] by FUNCT_2:def 1;

        

         A19: for x be object holds x in ( dom (G * (g,f))) iff x in ( dom h) & (h . x) in ( dom (G * (f,g)))

        proof

          let x be object;

          thus x in ( dom (G * (g,f))) implies x in ( dom h) & (h . x) in ( dom (G * (f,g)))

          proof

            assume

             A20: x in ( dom (G * (g,f)));

            then

            consider y,z be object such that

             A21: x = [y, z] by RELAT_1:def 1;

            

             A22: y in J & z in I by A17, A20, A21, ZFMISC_1: 87;

            then (h . (y,z)) = [z, y] by A2;

            hence thesis by A2, A18, A21, A22, ZFMISC_1: 87;

          end;

          assume that

           A23: x in ( dom h) and (h . x) in ( dom (G * (f,g)));

          thus thesis by A2, A23, FUNCT_2:def 1;

        end;

        for x be object st x in ( dom (G * (g,f))) holds ((G * (g,f)) . x) = ((G * (f,g)) . (h . x))

        proof

          let x be object;

          assume

           A24: x in ( dom (G * (g,f)));

          then

          consider y,z be object such that

           A25: x = [y, z] by RELAT_1:def 1;

          reconsider z as Element of I by A17, A24, A25, ZFMISC_1: 87;

          reconsider y as Element of J by A17, A24, A25, ZFMISC_1: 87;

          

           A26: [z, y] in ( dom (G * (f,g))) by A18, ZFMISC_1: 87;

          

           A27: [y, z] in ( dom (G * (g,f))) by A17, ZFMISC_1: 87;

          

          thus ((G * (f,g)) . (h . x)) = ((G * (f,g)) . (h . (y,z))) by A25

          .= ((G * (f,g)) . (z,y)) by A2

          .= (G . ((f . z),(g . y))) by A26, FINSEQOP: 77

          .= (G . ((g . y),(f . z))) by A15

          .= ((G * (g,f)) . (y,z)) by A27, FINSEQOP: 77

          .= ((G * (g,f)) . x) by A25;

        end;

        hence thesis by A19, FUNCT_1: 10;

      end;

      

       A28: X c= I & Y c= J by FINSUB_1:def 5;

      for y be object holds y in [:X, Y:] iff y in (h .: [:Y, X:])

      proof

        let y be object;

        thus y in [:X, Y:] implies y in (h .: [:Y, X:])

        proof

          assume

           A29: y in [:X, Y:];

          then

          consider y1,x1 be object such that

           A30: y = [y1, x1] by RELAT_1:def 1;

          

           A31: y1 in X & x1 in Y by A29, A30, ZFMISC_1: 87;

          then

           A32: [x1, y1] in [:Y, X:] & [x1, y1] in ( dom h) by A28, A2, ZFMISC_1: 87;

          (h . (x1,y1)) = y by A28, A2, A30, A31;

          hence thesis by A32, FUNCT_1:def 6;

        end;

        assume y in (h .: [:Y, X:]);

        then

        consider x be object such that x in ( dom h) and

         A33: x in [:Y, X:] and

         A34: y = (h . x) by FUNCT_1:def 6;

        consider x1,y1 be object such that

         A35: x = [x1, y1] by A33, RELAT_1:def 1;

        

         A36: x1 in Y & y1 in X by A33, A35, ZFMISC_1: 87;

        y = (h . (x1,y1)) by A34, A35;

        then y = [y1, x1] by A28, A2, A36;

        hence thesis by A36, ZFMISC_1: 87;

      end;

      then

       A37: (h .: [:Y, X:]) = [:X, Y:] by TARSKI: 2;

      reconsider h as Function of [:J, I:], [:I, J:] by A2, A11, FUNCT_2: 3;

      (F $$ ( [:X, Y:],(G * (f,g)))) = (F $$ ( [:Y, X:],((G * (f,g)) * h))) by A1, A10, A37, SETWOP_2: 6

      .= (F $$ ( [:Y, X:],(G * (g,f)))) by A16;

      hence thesis;

    end;

    theorem :: MATRIX_3:24

    

     Th24: for I,J be non empty set holds for F,G be BinOp of D holds for f be Function of I, D holds for g be Function of J, D st F is commutative & F is associative holds for x be Element of I holds for y be Element of J holds (F $$ ( [: {.x.}, {.y.}:],(G * (f,g)))) = (F $$ ( {.x.},(G [:] (f,(F $$ ( {.y.},g))))))

    proof

      let I,J be non empty set;

      let F,G be BinOp of D;

      let f be Function of I, D;

      let g be Function of J, D;

      assume

       A1: F is commutative & F is associative;

      reconsider G as Function of [:D, D:], D;

      

       A2: ( dom (G * (f,g))) = [:I, J:] by FUNCT_2:def 1;

      now

        let x be Element of I;

        let y be Element of J;

        

         A3: [x, y] in [:I, J:] by ZFMISC_1: 87;

        reconsider z = (g . y) as Element of D;

        reconsider u = [x, y] as Element of [:I, J:] by ZFMISC_1: 87;

        

         A4: ( dom <:f, (( dom f) --> z):>) = (( dom f) /\ ( dom (( dom f) --> z))) by FUNCT_3:def 7

        .= (( dom f) /\ ( dom f)) by FUNCOP_1: 13

        .= ( dom f);

        ( rng f) c= D & ( rng (( dom f) --> z)) c= D by RELAT_1:def 19;

        then

         A5: [:( rng f), ( rng (( dom f) --> z)):] c= [:D, D:] by ZFMISC_1: 96;

        ( dom f) = I by FUNCT_2:def 1;

        then

         A6: x in ( dom <:f, (( dom f) --> z):>) by A4;

        ( dom G) = [:D, D:] & ( rng <:f, (( dom f) --> z):>) c= [:( rng f), ( rng (( dom f) --> z)):] by FUNCT_2:def 1, FUNCT_3: 51;

        then x in ( dom (G * <:f, (( dom f) --> z):>)) by A6, A5, RELAT_1: 27, XBOOLE_1: 1;

        then

         A7: x in ( dom (G [:] (f,z))) by FUNCOP_1:def 4;

        

         A8: (F $$ ( {.x.},(G [:] (f,(F $$ ( {.y.},g)))))) = ((G [:] (f,(F $$ ( {.y.},g)))) . x) by A1, SETWISEO: 17

        .= ((G [:] (f,(g . y))) . x) by A1, SETWISEO: 17

        .= (G . ((f . x),(g . y))) by A7, FUNCOP_1: 27;

        (F $$ ( [: {.x.}, {.y.}:],(G * (f,g)))) = (F $$ ( {.u.},(G * (f,g)))) by ZFMISC_1: 29

        .= ((G * (f,g)) . (x,y)) by A1, SETWISEO: 17

        .= (G . ((f . x),(g . y))) by A2, A3, FINSEQOP: 77;

        hence (F $$ ( [: {.x.}, {.y.}:],(G * (f,g)))) = (F $$ ( {.x.},(G [:] (f,(F $$ ( {.y.},g)))))) by A8;

      end;

      hence thesis;

    end;

    theorem :: MATRIX_3:25

    

     Th25: for I,J be non empty set holds for F,G be BinOp of D holds for f be Function of I, D holds for g be Function of J, D holds for X be Element of ( Fin I) holds for Y be Element of ( Fin J) st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds for x be Element of I holds (F $$ ( [: {.x.}, Y:],(G * (f,g)))) = (F $$ ( {.x.},(G [:] (f,(F $$ (Y,g))))))

    proof

      let I,J be non empty set;

      let F,G be BinOp of D;

      let f be Function of I, D;

      let g be Function of J, D;

      let X be Element of ( Fin I);

      let Y be Element of ( Fin J);

      assume that

       A1: F is commutative and

       A2: F is associative and

       A3: F is having_a_unity and

       A4: F is having_an_inverseOp and

       A5: G is_distributive_wrt F;

      now

        let x be Element of I;

        defpred P[ Element of ( Fin J)] means (F $$ ( [: {.x.}, $1:],(G * (f,g)))) = (F $$ ( {.x.},(G [:] (f,(F $$ ($1,g))))));

        

         A6: P[( {}. J)]

        proof

          set z = ( the_unity_wrt F);

          reconsider T = ( {}. [:I, J:]) as Element of ( Fin [:I, J:]);

          

           A7: T = [: {x}, ( {}. J):] by ZFMISC_1: 90;

          

           A8: ( dom <:f, (( dom f) --> z):>) = (( dom f) /\ ( dom (( dom f) --> z))) by FUNCT_3:def 7

          .= (( dom f) /\ ( dom f)) by FUNCOP_1: 13

          .= ( dom f);

          ( rng f) c= D & ( rng (( dom f) --> z)) c= D by RELAT_1:def 19;

          then

           A9: [:( rng f), ( rng (( dom f) --> z)):] c= [:D, D:] by ZFMISC_1: 96;

          ( dom f) = I by FUNCT_2:def 1;

          then

           A10: x in ( dom <:f, (( dom f) --> z):>) by A8;

          ( dom G) = [:D, D:] & ( rng <:f, (( dom f) --> z):>) c= [:( rng f), ( rng (( dom f) --> z)):] by FUNCT_2:def 1, FUNCT_3: 51;

          then x in ( dom (G * <:f, (( dom f) --> z):>)) by A10, A9, RELAT_1: 27, XBOOLE_1: 1;

          then

           A11: x in ( dom (G [:] (f,z))) by FUNCOP_1:def 4;

          (F $$ ( {.x.},(G [:] (f,(F $$ (( {}. J),g)))))) = (F $$ ( {.x.},(G [:] (f,( the_unity_wrt F))))) by A1, A2, A3, SETWISEO: 31

          .= ((G [:] (f,( the_unity_wrt F))) . x) by A1, A2, SETWISEO: 17

          .= (G . ((f . x),( the_unity_wrt F))) by A11, FUNCOP_1: 27

          .= ( the_unity_wrt F) by A2, A3, A4, A5, FINSEQOP: 66;

          hence thesis by A1, A2, A3, A7, SETWISEO: 31;

        end;

        

         A12: for Y1 be Element of ( Fin J), y be Element of J st P[Y1] holds P[(Y1 \/ {.y.})]

        proof

          let Y1 be Element of ( Fin J), y be Element of J;

          assume

           A13: (F $$ ( [: {.x.}, Y1:],(G * (f,g)))) = (F $$ ( {.x.},(G [:] (f,(F $$ (Y1,g))))));

          reconsider s = {.y.} as Element of ( Fin J);

          per cases ;

            suppose y in Y1;

            then (Y1 \/ {y}) = Y1 by ZFMISC_1: 40;

            hence thesis by A13;

          end;

            suppose not y in Y1;

            then

             A14: Y1 misses {y} by ZFMISC_1: 50;

            then

             A15: [: {x}, Y1:] misses [: {x}, s:] by ZFMISC_1: 104;

            

            thus (F $$ ( [: {.x.}, (Y1 \/ {.y.}):],(G * (f,g)))) = (F $$ (( [: {.x.}, Y1:] \/ [: {.x.}, s:]),(G * (f,g)))) by ZFMISC_1: 97

            .= (F . ((F $$ ( [: {.x.}, Y1:],(G * (f,g)))),(F $$ ( [: {.x.}, s:],(G * (f,g)))))) by A1, A2, A3, A15, SETWOP_2: 4

            .= (F . ((F $$ ( {.x.},(G [:] (f,(F $$ (Y1,g)))))),(F $$ ( {.x.},(G [:] (f,(F $$ (s,g)))))))) by A1, A2, A13, Th24

            .= (F $$ ( {.x.},(F .: ((G [:] (f,(F $$ (Y1,g)))),(G [:] (f,(F $$ (s,g)))))))) by A1, A2, A3, SETWOP_2: 10

            .= (F $$ ( {.x.},(G [:] (f,(F . ((F $$ (Y1,g)),(F $$ (s,g)))))))) by A5, FINSEQOP: 36

            .= (F $$ ( {.x.},(G [:] (f,(F $$ ((Y1 \/ {.y.}),g)))))) by A1, A2, A3, A14, SETWOP_2: 4;

          end;

        end;

        thus for Y be Element of ( Fin J) holds P[Y] from SETWISEO:sch 4( A6, A12);

      end;

      hence thesis;

    end;

    theorem :: MATRIX_3:26

    

     Th26: for I,J be non empty set holds for F,G be BinOp of D holds for f be Function of I, D holds for g be Function of J, D holds for X be Element of ( Fin I) holds for Y be Element of ( Fin J) st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds (F $$ ( [:X, Y:],(G * (f,g)))) = (F $$ (X,(G [:] (f,(F $$ (Y,g))))))

    proof

      let I,J be non empty set;

      let F,G be BinOp of D;

      let f be Function of I, D;

      let g be Function of J, D;

      let X be Element of ( Fin I);

      let Y be Element of ( Fin J);

      assume that

       A1: F is having_a_unity & F is commutative & F is associative and

       A2: F is having_an_inverseOp & G is_distributive_wrt F;

      defpred P[ Element of ( Fin I)] means (F $$ ( [:$1, Y:],(G * (f,g)))) = (F $$ ($1,(G [:] (f,(F $$ (Y,g))))));

      

       A3: for X1 be Element of ( Fin I), x be Element of I st P[X1] holds P[(X1 \/ {.x.})]

      proof

        let X1 be Element of ( Fin I), x be Element of I;

        reconsider s = {.x.} as Element of ( Fin I);

        assume

         A4: (F $$ ( [:X1, Y:],(G * (f,g)))) = (F $$ (X1,(G [:] (f,(F $$ (Y,g))))));

        now

          per cases ;

            case x in X1;

            then (X1 \/ {x}) = X1 by ZFMISC_1: 40;

            hence thesis by A4;

          end;

            case not x in X1;

            then

             A5: X1 misses {x} by ZFMISC_1: 50;

            then

             A6: [:X1, Y:] misses [:s, Y:] by ZFMISC_1: 104;

            

            thus (F $$ ( [:(X1 \/ {.x.}), Y:],(G * (f,g)))) = (F $$ (( [:X1, Y:] \/ [:s, Y:]),(G * (f,g)))) by ZFMISC_1: 97

            .= (F . ((F $$ ( [:X1, Y:],(G * (f,g)))),(F $$ ( [:s, Y:],(G * (f,g)))))) by A1, A6, SETWOP_2: 4

            .= (F . ((F $$ (X1,(G [:] (f,(F $$ (Y,g)))))),(F $$ (s,(G [:] (f,(F $$ (Y,g)))))))) by A1, A2, A4, Th25

            .= (F $$ ((X1 \/ {.x.}),(G [:] (f,(F $$ (Y,g)))))) by A1, A5, SETWOP_2: 4;

          end;

        end;

        hence thesis;

      end;

      

       A7: P[( {}. I)]

      proof

        reconsider T = ( {}. [:I, J:]) as Element of ( Fin [:I, J:]);

        T = [:( {}. I), Y:] by ZFMISC_1: 90;

        then (F $$ ( [:( {}. I), Y:],(G * (f,g)))) = ( the_unity_wrt F) by A1, SETWISEO: 31;

        hence thesis by A1, SETWISEO: 31;

      end;

      for X1 be Element of ( Fin I) holds P[X1] from SETWISEO:sch 4( A7, A3);

      hence thesis;

    end;

    theorem :: MATRIX_3:27

    for I,J be non empty set holds for F,G be BinOp of D holds for f be Function of I, D holds for g be Function of J, D st F is commutative associative & G is commutative holds for x be Element of I holds for y be Element of J holds (F $$ ( [: {.x.}, {.y.}:],(G * (f,g)))) = (F $$ ( {.y.},(G [;] ((F $$ ( {.x.},f)),g))))

    proof

      let I,J be non empty set;

      let F,G be BinOp of D;

      let f be Function of I, D;

      let g be Function of J, D;

      assume that

       A1: F is commutative associative and

       A2: G is commutative;

      now

        let x be Element of I;

        let y be Element of J;

        

        thus (F $$ ( [: {.x.}, {.y.}:],(G * (f,g)))) = (F $$ ( [: {.y.}, {.x.}:],(G * (g,f)))) by A1, A2, Th23

        .= (F $$ ( {.y.},(G [:] (g,(F $$ ( {.x.},f)))))) by A1, Th24

        .= (F $$ ( {.y.},(G [;] ((F $$ ( {.x.},f)),g)))) by A2, FUNCOP_1: 64;

      end;

      hence thesis;

    end;

    theorem :: MATRIX_3:28

    for I,J be non empty set holds for F,G be BinOp of D holds for f be Function of I, D holds for g be Function of J, D holds for X be Element of ( Fin I) holds for Y be Element of ( Fin J) st F is having_a_unity & F is commutative associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds (F $$ ( [:X, Y:],(G * (f,g)))) = (F $$ (Y,(G [;] ((F $$ (X,f)),g))))

    proof

      let I,J be non empty set;

      let F,G be BinOp of D;

      let f be Function of I, D;

      let g be Function of J, D;

      let X be Element of ( Fin I);

      let Y be Element of ( Fin J);

      assume that

       A1: F is having_a_unity & F is commutative & F is associative and

       A2: F is having_an_inverseOp & G is_distributive_wrt F and

       A3: G is commutative;

      

      thus (F $$ ( [:X, Y:],(G * (f,g)))) = (F $$ ( [:Y, X:],(G * (g,f)))) by A1, A3, Th23

      .= (F $$ (Y,(G [:] (g,(F $$ (X,f)))))) by A1, A2, Th26

      .= (F $$ (Y,(G [;] ((F $$ (X,f)),g)))) by A3, FUNCOP_1: 64;

    end;

    theorem :: MATRIX_3:29

    

     Th29: for I,J be non empty set holds for F be BinOp of D holds for f be Function of [:I, J:], D holds for g be Function of I, D holds for Y be Element of ( Fin J) st F is having_a_unity commutative associative holds for x be Element of I holds (for i be Element of I holds (g . i) = (F $$ (Y,(( curry f) . i)))) implies (F $$ ( [: {.x.}, Y:],f)) = (F $$ ( {.x.},g))

    proof

      let I,J be non empty set;

      let F be BinOp of D;

      let f be Function of [:I, J:], D;

      let g be Function of I, D;

      let Y be Element of ( Fin J);

      assume that

       A1: F is having_a_unity and

       A2: F is commutative & F is associative;

      now

        let x be Element of I;

        assume

         A3: for i be Element of I holds (g . i) = (F $$ (Y,(( curry f) . i)));

        deffunc F( object) = [x, $1];

        consider h be Function such that

         A4: ( dom h) = J & for y be object st y in J holds (h . y) = F(y) from FUNCT_1:sch 3;

        

         A5: ( dom (( curry f) . x)) = J & ( dom (f * h)) = J & ( rng h) c= [:I, J:]

        proof

          

           A6: ( dom f) = [:I, J:] by FUNCT_2:def 1;

          then ex g be Function st g = (( curry f) . x) & ( dom g) = J & ( rng g) c= ( rng f) & for y st y in J holds (g . y) = (f . (x,y)) by FUNCT_5: 29;

          hence ( dom (( curry f) . x)) = J;

          now

            let y be object;

            assume y in ( rng h);

            then

            consider z be object such that

             A7: z in ( dom h) and

             A8: y = (h . z) by FUNCT_1:def 3;

            y = [x, z] by A4, A7, A8;

            hence y in ( dom f) by A4, A6, A7, ZFMISC_1: 87;

          end;

          then ( rng h) c= ( dom f) by TARSKI:def 3;

          hence thesis by A4, FUNCT_2:def 1, RELAT_1: 27;

        end;

        

         A9: for y be object st y in J holds ((( curry f) . x) . y) = ((f * h) . y)

        proof

          let y be object;

          ( dom f) = [:I, J:] by FUNCT_2:def 1;

          then

           A10: ex g be Function st g = (( curry f) . x) & ( dom g) = J & ( rng g) c= ( rng f) & for y st y in J holds (g . y) = (f . (x,y)) by FUNCT_5: 29;

          assume

           A11: y in J;

          

          hence ((f * h) . y) = (f . (h . y)) by A5, FUNCT_1: 12

          .= (f . (x,y)) by A4, A11

          .= ((( curry f) . x) . y) by A11, A10;

        end;

        for y be object holds y in [: {x}, Y:] iff y in (h .: Y)

        proof

          let y be object;

          thus y in [: {x}, Y:] implies y in (h .: Y)

          proof

            assume

             A12: y in [: {x}, Y:];

            then

            consider y1,x1 be object such that

             A13: y = [y1, x1] by RELAT_1:def 1;

            

             A14: y1 in {x} by A12, A13, ZFMISC_1: 87;

            

             A15: Y c= J & x1 in Y by A12, A13, FINSUB_1:def 5, ZFMISC_1: 87;

            

            then (h . x1) = [x, x1] by A4

            .= y by A13, A14, TARSKI:def 1;

            hence thesis by A4, A15, FUNCT_1:def 6;

          end;

          assume y in (h .: Y);

          then

          consider z be object such that

           A16: z in ( dom h) and

           A17: z in Y and

           A18: y = (h . z) by FUNCT_1:def 6;

          y = [x, z] by A4, A16, A18;

          hence thesis by A17, ZFMISC_1: 105;

        end;

        then

         A19: (h .: Y) = [: {x}, Y:] by TARSKI: 2;

        now

          let x1,x2 be object;

          assume that

           A20: x1 in ( dom h) and

           A21: x2 in ( dom h) and

           A22: (h . x1) = (h . x2);

           [x, x1] = (h . x2) by A4, A20, A22

          .= [x, x2] by A4, A21;

          hence x1 = x2 by XTUPLE_0: 1;

        end;

        then

         A23: h is one-to-one by FUNCT_1:def 4;

        reconsider h as Function of J, [:I, J:] by A4, A5, FUNCT_2: 2;

        

        thus (F $$ ( [: {.x.}, Y:],f)) = (F $$ (Y,(f * h))) by A1, A2, A23, A19, SETWOP_2: 6

        .= (F $$ (Y,(( curry f) . x))) by A5, A9, FUNCT_1: 2

        .= (g . x) by A3

        .= (F $$ ( {.x.},g)) by A2, SETWISEO: 17;

      end;

      hence thesis;

    end;

    theorem :: MATRIX_3:30

    

     Th30: for I,J be non empty set holds for F be BinOp of D holds for f be Function of [:I, J:], D holds for g be Function of I, D holds for X be Element of ( Fin I) holds for Y be Element of ( Fin J) st (for i be Element of I holds (g . i) = (F $$ (Y,(( curry f) . i)))) & F is having_a_unity & F is commutative & F is associative holds (F $$ ( [:X, Y:],f)) = (F $$ (X,g))

    proof

      let I,J be non empty set;

      let F be BinOp of D;

      let f be Function of [:I, J:], D;

      let g be Function of I, D;

      let X be Element of ( Fin I);

      let Y be Element of ( Fin J);

      assume that

       A1: for i be Element of I holds (g . i) = (F $$ (Y,(( curry f) . i))) and

       A2: F is having_a_unity & F is commutative & F is associative;

      defpred P[ Element of ( Fin I)] means (F $$ ( [:$1, Y:],f)) = (F $$ ($1,g));

      

       A3: for X1 be Element of ( Fin I), x be Element of I holds P[X1] implies P[(X1 \/ {.x.})]

      proof

        let X1 be Element of ( Fin I), x be Element of I;

        assume

         A4: (F $$ ( [:X1, Y:],f)) = (F $$ (X1,g));

        reconsider s = {.x.} as Element of ( Fin I);

        per cases ;

          suppose x in X1;

          then (X1 \/ {x}) = X1 by ZFMISC_1: 40;

          hence thesis by A4;

        end;

          suppose not x in X1;

          then

           A5: X1 misses {x} by ZFMISC_1: 50;

          then

           A6: [:X1, Y:] misses [:s, Y:] by ZFMISC_1: 104;

          

          thus (F $$ ( [:(X1 \/ {.x.}), Y:],f)) = (F $$ (( [:X1, Y:] \/ [:s, Y:]),f)) by ZFMISC_1: 97

          .= (F . ((F $$ ( [:X1, Y:],f)),(F $$ ( [:s, Y:],f)))) by A2, A6, SETWOP_2: 4

          .= (F . ((F $$ (X1,g)),(F $$ (s,g)))) by A1, A2, A4, Th29

          .= (F $$ ((X1 \/ {.x.}),g)) by A2, A5, SETWOP_2: 4;

        end;

      end;

      

       A7: P[( {}. I)]

      proof

        reconsider T = ( {}. [:I, J:]) as Element of ( Fin [:I, J:]);

        T = [:( {}. I), Y:] by ZFMISC_1: 90;

        then (F $$ ( [:( {}. I), Y:],f)) = ( the_unity_wrt F) by A2, SETWISEO: 31;

        hence thesis by A2, SETWISEO: 31;

      end;

      for X1 be Element of ( Fin I) holds P[X1] from SETWISEO:sch 4( A7, A3);

      hence thesis;

    end;

    theorem :: MATRIX_3:31

    

     Th31: for I,J be non empty set holds for F be BinOp of D holds for f be Function of [:I, J:], D holds for g be Function of J, D holds for X be Element of ( Fin I) st F is having_a_unity & F is commutative & F is associative holds for y be Element of J holds (for j be Element of J holds (g . j) = (F $$ (X,(( curry' f) . j)))) implies (F $$ ( [:X, {.y.}:],f)) = (F $$ ( {.y.},g))

    proof

      let I,J be non empty set;

      let F be BinOp of D;

      let f be Function of [:I, J:], D;

      let g be Function of J, D;

      let X be Element of ( Fin I);

      assume that

       A1: F is having_a_unity and

       A2: F is commutative & F is associative;

      now

        let y be Element of J;

        assume

         A3: for j be Element of J holds (g . j) = (F $$ (X,(( curry' f) . j)));

        deffunc F( object) = [$1, y];

        consider h be Function such that

         A4: ( dom h) = I & for x be object st x in I holds (h . x) = F(x) from FUNCT_1:sch 3;

        

         A5: ( dom (( curry' f) . y)) = I & ( dom (f * h)) = I & ( rng h) c= [:I, J:]

        proof

          

           A6: ( dom f) = [:I, J:] by FUNCT_2:def 1;

          then ex g be Function st g = (( curry' f) . y) & ( dom g) = I & ( rng g) c= ( rng f) & for x st x in I holds (g . x) = (f . (x,y)) by FUNCT_5: 32;

          hence ( dom (( curry' f) . y)) = I;

          now

            let x be object;

            assume x in ( rng h);

            then

            consider z be object such that

             A7: z in ( dom h) and

             A8: x = (h . z) by FUNCT_1:def 3;

            x = [z, y] by A4, A7, A8;

            hence x in ( dom f) by A4, A6, A7, ZFMISC_1: 87;

          end;

          then ( rng h) c= ( dom f) by TARSKI:def 3;

          hence thesis by A4, FUNCT_2:def 1, RELAT_1: 27;

        end;

        

         A9: for x be object st x in I holds ((( curry' f) . y) . x) = ((f * h) . x)

        proof

          let x be object;

          ( dom f) = [:I, J:] by FUNCT_2:def 1;

          then

           A10: ex g be Function st g = (( curry' f) . y) & ( dom g) = I & ( rng g) c= ( rng f) & for x st x in I holds (g . x) = (f . (x,y)) by FUNCT_5: 32;

          assume

           A11: x in I;

          

          hence ((f * h) . x) = (f . (h . x)) by A5, FUNCT_1: 12

          .= (f . (x,y)) by A4, A11

          .= ((( curry' f) . y) . x) by A11, A10;

        end;

        for x be object holds x in [:X, {y}:] iff x in (h .: X)

        proof

          let x be object;

          thus x in [:X, {y}:] implies x in (h .: X)

          proof

            assume

             A12: x in [:X, {y}:];

            then

            consider x1,y1 be object such that

             A13: x = [x1, y1] by RELAT_1:def 1;

            

             A14: y1 in {y} by A12, A13, ZFMISC_1: 87;

            

             A15: X c= I & x1 in X by A12, A13, FINSUB_1:def 5, ZFMISC_1: 87;

            

            then (h . x1) = [x1, y] by A4

            .= x by A13, A14, TARSKI:def 1;

            hence thesis by A4, A15, FUNCT_1:def 6;

          end;

          assume x in (h .: X);

          then

          consider z be object such that

           A16: z in ( dom h) and

           A17: z in X and

           A18: x = (h . z) by FUNCT_1:def 6;

          x = [z, y] by A4, A16, A18;

          hence thesis by A17, ZFMISC_1: 106;

        end;

        then

         A19: (h .: X) = [:X, {y}:] by TARSKI: 2;

        now

          let x1,x2 be object;

          assume that

           A20: x1 in ( dom h) and

           A21: x2 in ( dom h) and

           A22: (h . x1) = (h . x2);

           [x1, y] = (h . x2) by A4, A20, A22

          .= [x2, y] by A4, A21;

          hence x1 = x2 by XTUPLE_0: 1;

        end;

        then

         A23: h is one-to-one by FUNCT_1:def 4;

        reconsider h as Function of I, [:I, J:] by A4, A5, FUNCT_2: 2;

        

        thus (F $$ ( [:X, {.y.}:],f)) = (F $$ (X,(f * h))) by A1, A2, A23, A19, SETWOP_2: 6

        .= (F $$ (X,(( curry' f) . y))) by A5, A9, FUNCT_1: 2

        .= (g . y) by A3

        .= (F $$ ( {.y.},g)) by A2, SETWISEO: 17;

      end;

      hence thesis;

    end;

    theorem :: MATRIX_3:32

    

     Th32: for I,J be non empty set holds for F be BinOp of D holds for f be Function of [:I, J:], D holds for g be Function of J, D holds for X be Element of ( Fin I) holds for Y be Element of ( Fin J) st (for j be Element of J holds (g . j) = (F $$ (X,(( curry' f) . j)))) & F is having_a_unity & F is commutative & F is associative holds (F $$ ( [:X, Y:],f)) = (F $$ (Y,g))

    proof

      let I,J be non empty set;

      let F be BinOp of D;

      let f be Function of [:I, J:], D;

      let g be Function of J, D;

      let X be Element of ( Fin I);

      let Y be Element of ( Fin J);

      assume that

       A1: for j be Element of J holds (g . j) = (F $$ (X,(( curry' f) . j))) and

       A2: F is having_a_unity & F is commutative & F is associative;

      defpred P[ Element of ( Fin J)] means (F $$ ( [:X, $1:],f)) = (F $$ ($1,g));

      

       A3: for Y1 be Element of ( Fin J), y be Element of J holds P[Y1] implies P[(Y1 \/ {.y.})]

      proof

        let Y1 be Element of ( Fin J), y be Element of J;

        assume

         A4: (F $$ ( [:X, Y1:],f)) = (F $$ (Y1,g));

        reconsider s = {.y.} as Element of ( Fin J);

        per cases ;

          suppose y in Y1;

          then (Y1 \/ {y}) = Y1 by ZFMISC_1: 40;

          hence thesis by A4;

        end;

          suppose not y in Y1;

          then

           A5: Y1 misses {y} by ZFMISC_1: 50;

          then

           A6: [:X, Y1:] misses [:X, s:] by ZFMISC_1: 104;

          

          thus (F $$ ( [:X, (Y1 \/ {.y.}):],f)) = (F $$ (( [:X, Y1:] \/ [:X, s:]),f)) by ZFMISC_1: 97

          .= (F . ((F $$ ( [:X, Y1:],f)),(F $$ ( [:X, s:],f)))) by A2, A6, SETWOP_2: 4

          .= (F . ((F $$ (Y1,g)),(F $$ (s,g)))) by A1, A2, A4, Th31

          .= (F $$ ((Y1 \/ {.y.}),g)) by A2, A5, SETWOP_2: 4;

        end;

      end;

      

       A7: P[( {}. J)]

      proof

        reconsider T = ( {}. [:I, J:]) as Element of ( Fin [:I, J:]);

        T = [:X, ( {}. J):] by ZFMISC_1: 90;

        then (F $$ ( [:X, ( {}. J):],f)) = ( the_unity_wrt F) by A2, SETWISEO: 31;

        hence thesis by A2, SETWISEO: 31;

      end;

      for Y1 be Element of ( Fin J) holds P[Y1] from SETWISEO:sch 4( A7, A3);

      hence thesis;

    end;

    theorem :: MATRIX_3:33

    for K be commutative Ring holds for A,B,C be Matrix of K st ( width A) = ( len B) & ( width B) = ( len C) holds ((A * B) * C) = (A * (B * C))

    proof

      let K be commutative Ring;

      let A,B,C be Matrix of K;

      assume that

       A1: ( width A) = ( len B) and

       A2: ( width B) = ( len C);

      

       A3: ( len (B * C)) = ( width A) by A1, A2, Def4;

      

       A4: ( width (B * C)) = ( width C) by A2, Def4;

      then

       A5: ( width (A * (B * C))) = ( width C) by A3, Def4;

      ( dom (B * C)) = ( dom B) by A1, A3, FINSEQ_3: 29;

      then

       A6: ( Indices (B * C)) = [:( dom B), ( Seg ( width C)):] by A4;

      

       A7: ( Seg ( len B)) = ( dom B) by FINSEQ_1:def 3;

      

       A8: ( len (A * (B * C))) = ( len A) by A3, Def4;

      then ( dom (A * (B * C))) = ( dom A) by FINSEQ_3: 29;

      then

       A9: ( Indices (A * (B * C))) = [:( dom A), ( Seg ( width C)):] by A5;

      ( 0. K) is_a_unity_wrt the addF of K by FVSUM_1: 6;

      then

       A10: the addF of K is having_a_unity by SETWISEO:def 2;

      

       A11: ( width (A * B)) = ( len C) by A1, A2, Def4;

      then

       A12: ( width ((A * B) * C)) = ( width C) by Def4;

      

       A13: ( len (A * B)) = ( len A) by A1, Def4;

      then ( dom (A * B)) = ( dom A) by FINSEQ_3: 29;

      then

       A14: ( Indices (A * B)) = [:( dom A), ( Seg ( width B)):] by A2, A11;

      

       A15: ( len ((A * B) * C)) = ( len A) by A13, A11, Def4;

      then

       A16: ( dom ((A * B) * C)) = ( dom A) by FINSEQ_3: 29;

      then

       A17: ( Indices ((A * B) * C)) = [:( dom A), ( Seg ( width C)):] by A12;

      

       A18: ( Indices ((A * B) * C)) = [:( dom A), ( Seg ( width C)):] by A12, A16;

      now

        reconsider Y = ( findom B) as Element of ( Fin NAT );

        reconsider X = ( findom C) as Element of ( Fin NAT );

        let i, j;

        deffunc F( Element of NAT , Element of NAT ) = (((A * (i,$2)) * (B * ($2,$1))) * (C * ($1,j)));

        consider f be Function of [: NAT , NAT :], the carrier of K such that

         A19: for k1 be Element of NAT holds for k2 be Element of NAT holds (f . (k1,k2)) = F(k1,k2) from BINOP_1:sch 4;

        

         A20: for k be Element of NAT st k in NAT holds ((( curry f) . k) | ( dom B)) = ((C * (k,j)) * ( mlt (( Line (A,i)),( Col (B,k)))))

        proof

          let k be Element of NAT ;

          assume k in NAT ;

          

           A21: {k} c= NAT by ZFMISC_1: 31;

          reconsider a = (C * (k,j)) as Element of K;

          

           A22: ( dom ( curry f)) = NAT by FUNCT_2:def 1;

          ( dom f) = [: NAT , NAT :] by FUNCT_2:def 1;

          

          then

           A23: ( dom (( curry f) . k)) = ( proj2 ( [: NAT , NAT :] /\ [: {k}, ( proj2 [: NAT , NAT :]):])) by A22, FUNCT_5: 31

          .= ( proj2 ( [: {k}, NAT :] /\ [: NAT , NAT :])) by FUNCT_5: 9

          .= ( proj2 [: {k}, NAT :]) by A21, ZFMISC_1: 101

          .= NAT by FUNCT_5: 9;

          

          then

           A24: ( dom ((( curry f) . k) | ( dom B))) = ( NAT /\ ( dom B)) by RELAT_1: 61

          .= ( dom B) by XBOOLE_1: 28;

          reconsider p = ( mlt (( Line (A,i)),( Col (B,k)))) as FinSequence of K;

          

           A25: ( len ( mlt (( Line (A,i)),( Col (B,k))))) = ( len (the multF of K .: (( Line (A,i)),( Col (B,k))))) by FVSUM_1:def 7;

          ( len ( Line (A,i))) = ( len B) by A1, MATRIX_0:def 7

          .= ( len ( Col (B,k))) by MATRIX_0:def 8;

          

          then

           A26: ( len (the multF of K .: (( Line (A,i)),( Col (B,k))))) = ( len ( Line (A,i))) by FINSEQ_2: 72

          .= ( len B) by A1, MATRIX_0:def 7;

          ( dom (a multfield )) = the carrier of K by FUNCT_2:def 1;

          then (a * p) = ((a multfield ) * p) & ( rng p) c= ( dom (a multfield )) by FINSEQ_1:def 4, FVSUM_1:def 6;

          then

           A27: ( dom (a * p)) = ( dom p) by RELAT_1: 27;

          

           A28: ( dom (the multF of K .: (( Line (A,i)),( Col (B,k))))) = ( Seg ( len (the multF of K .: (( Line (A,i)),( Col (B,k)))))) by FINSEQ_1:def 3;

           A29:

          now

            let l be object;

            assume

             A30: l in ( dom B);

            then

            reconsider l9 = l as Element of NAT ;

            

             A31: l in ( dom (a * p)) by A25, A26, A27, A30, FINSEQ_3: 29;

            l9 in ( dom p) by A25, A26, A30, FINSEQ_3: 29;

            then

            reconsider b = (p . l9) as Element of K by FINSEQ_2: 11;

            

             A32: l9 in ( dom (the multF of K .: (( Line (A,i)),( Col (B,k))))) by A26, A28, A30, FINSEQ_1:def 3;

            

            thus (((( curry f) . k) | ( dom B)) . l) = ((( curry f) . k) . l9) by A30, FUNCT_1: 49

            .= (f . (k,l9)) by A22, A23, FUNCT_5: 31

            .= (((A * (i,l9)) * (B * (l9,k))) * (C * (k,j))) by A19

            .= (the multF of K . ((the multF of K . ((( Line (A,i)) . l9),(B * (l9,k)))),(C * (k,j)))) by A1, A7, A30, MATRIX_0:def 7

            .= (the multF of K . ((the multF of K . ((( Line (A,i)) . l9),(( Col (B,k)) . l9))),(C * (k,j)))) by A30, MATRIX_0:def 8

            .= (the multF of K . (((the multF of K .: (( Line (A,i)),( Col (B,k)))) . l9),(C * (k,j)))) by A32, FUNCOP_1: 22

            .= (b * a) by FVSUM_1:def 7

            .= (((C * (k,j)) * ( mlt (( Line (A,i)),( Col (B,k))))) . l) by A31, FVSUM_1: 50;

          end;

          ( dom ((C * (k,j)) * ( mlt (( Line (A,i)),( Col (B,k)))))) = ( dom B) by A25, A26, A27, FINSEQ_3: 29;

          hence thesis by A24, A29, FUNCT_1: 2;

        end;

        

         A33: ( 0. K) = ( the_unity_wrt the addF of K) by FVSUM_1: 7;

        deffunc F9( Element of NAT ) = (the addF of K $$ (X,(( curry' f) . $1)));

        deffunc F( Element of NAT ) = (the addF of K $$ (Y,(( curry f) . $1)));

        consider g be sequence of the carrier of K such that

         A34: for k be Element of NAT holds (g . k) = F(k) from FUNCT_2:sch 4;

        

         A35: ( dom (g | ( dom C))) = (( dom g) /\ ( dom C)) by RELAT_1: 61

        .= ( NAT /\ ( dom C)) by FUNCT_2:def 1

        .= ( dom C) by XBOOLE_1: 28;

        ( len ( Line ((A * B),i))) = ( width (A * B)) by MATRIX_0:def 7

        .= ( len C) by A1, A2, Def4

        .= ( len ( Col (C,j))) by MATRIX_0:def 8;

        

        then

         A36: ( len (the multF of K .: (( Line ((A * B),i)),( Col (C,j))))) = ( len ( Col (C,j))) by FINSEQ_2: 72

        .= ( len C) by MATRIX_0:def 8;

        assume

         A37: [i, j] in ( Indices ((A * B) * C));

        then

         A38: i in ( dom A) by A17, ZFMISC_1: 87;

         A39:

        now

          let k9 be object;

          assume

           A40: k9 in ( dom C);

          then

          reconsider k = k9 as Element of NAT ;

          

           A41: k in ( dom (the multF of K .: (( Line ((A * B),i)),( Col (C,j))))) by A36, A40, FINSEQ_3: 29;

          reconsider p = ( mlt (( Line (A,i)),( Col (B,k)))) as FinSequence of K;

          reconsider a = (C * (k,j)) as Element of K;

          ( dom (a multfield )) = the carrier of K by FUNCT_2:def 1;

          then (a * p) = ((a multfield ) * p) & ( rng p) c= ( dom (a multfield )) by FINSEQ_1:def 4, FVSUM_1:def 6;

          then

           A42: ( dom (a * p)) = ( dom p) by RELAT_1: 27;

          ( len ( Line (A,i))) = ( len B) by A1, MATRIX_0:def 7

          .= ( len ( Col (B,k))) by MATRIX_0:def 8;

          

          then ( len (the multF of K .: (( Line (A,i)),( Col (B,k))))) = ( len ( Line (A,i))) by FINSEQ_2: 72

          .= ( len B) by A1, MATRIX_0:def 7;

          then ( len B) = ( len p) by FVSUM_1:def 7;

          then

           A43: ( dom ((C * (k,j)) * ( mlt (( Line (A,i)),( Col (B,k)))))) = ( dom B) by A42, FINSEQ_3: 29;

          then (( [#] (((C * (k,j)) * ( mlt (( Line (A,i)),( Col (B,k))))),( 0. K))) | ( dom B)) = ((C * (k,j)) * ( mlt (( Line (A,i)),( Col (B,k))))) by SETWOP_2: 21;

          then

           A44: (( [#] (((C * (k,j)) * ( mlt (( Line (A,i)),( Col (B,k))))),( 0. K))) | ( dom B)) = ((( curry f) . k) | ( dom B)) by A20;

          k in ( Seg ( width B)) by A2, A40, FINSEQ_1:def 3;

          then

           A45: [i, k] in ( Indices (A * B)) by A14, A38, ZFMISC_1: 87;

          

           A46: k in ( Seg ( width (A * B))) by A11, A40, FINSEQ_1:def 3;

          

          thus ((g | ( dom C)) . k9) = (g . k) by A35, A40, FUNCT_1: 47

          .= (the addF of K $$ (Y,(( curry f) . k))) by A34

          .= (the addF of K $$ (Y,( [#] (((C * (k,j)) * ( mlt (( Line (A,i)),( Col (B,k))))),( 0. K))))) by A44, FVSUM_1: 8, SETWOP_2: 7

          .= (the addF of K $$ (a * p)) by A10, A33, A43, SETWOP_2:def 2

          .= ( Sum (a * p)) by FVSUM_1:def 8

          .= ((C * (k,j)) * ( Sum ( mlt (( Line (A,i)),( Col (B,k)))))) by FVSUM_1: 73

          .= ((C * (k,j)) * (( Line (A,i)) "*" ( Col (B,k)))) by FVSUM_1:def 9

          .= (((A * B) * (i,k)) * (C * (k,j))) by A1, A45, Def4

          .= (the multF of K . ((( Line ((A * B),i)) . k),(C * (k,j)))) by A46, MATRIX_0:def 7

          .= (the multF of K . ((( Line ((A * B),i)) . k),(( Col (C,j)) . k))) by A40, MATRIX_0:def 8

          .= ((the multF of K .: (( Line ((A * B),i)),( Col (C,j)))) . k) by A41, FUNCOP_1: 22

          .= (( mlt (( Line ((A * B),i)),( Col (C,j)))) . k9) by FVSUM_1:def 7;

        end;

        

         A47: ( len (the multF of K .: (( Line ((A * B),i)),( Col (C,j))))) = ( len ( mlt (( Line ((A * B),i)),( Col (C,j))))) by FVSUM_1:def 7;

        then

         A48: ( dom C) = ( dom ( mlt (( Line ((A * B),i)),( Col (C,j))))) by A36, FINSEQ_3: 29;

        ( dom ( mlt (( Line ((A * B),i)),( Col (C,j))))) = ( dom C) by A36, A47, FINSEQ_3: 29;

        then

         A49: (( [#] (( mlt (( Line ((A * B),i)),( Col (C,j)))),( 0. K))) | ( dom C)) = ( mlt (( Line ((A * B),i)),( Col (C,j)))) by SETWOP_2: 21;

        ( len ( Col ((B * C),j))) = ( len (B * C)) by MATRIX_0:def 8

        .= ( width A) by A1, A2, Def4

        .= ( len ( Line (A,i))) by MATRIX_0:def 7;

        

        then

         A50: ( len (the multF of K .: (( Line (A,i)),( Col ((B * C),j))))) = ( len ( Line (A,i))) by FINSEQ_2: 72

        .= ( width A) by MATRIX_0:def 7;

        

         A51: ( len (the multF of K .: (( Line (A,i)),( Col ((B * C),j))))) = ( len ( mlt (( Line (A,i)),( Col ((B * C),j))))) by FVSUM_1:def 7;

        then

         A52: ( dom ( mlt (( Line (A,i)),( Col ((B * C),j))))) = Y by A1, A50, FINSEQ_3: 29;

        ( dom ( mlt (( Line (A,i)),( Col ((B * C),j))))) = ( dom B) by A1, A50, A51, FINSEQ_3: 29;

        then

         A53: (( [#] (( mlt (( Line (A,i)),( Col ((B * C),j)))),( 0. K))) | ( dom B)) = ( mlt (( Line (A,i)),( Col ((B * C),j)))) by SETWOP_2: 21;

        consider h be sequence of the carrier of K such that

         A54: for k be Element of NAT holds (h . k) = F9(k) from FUNCT_2:sch 4;

        

         A55: ( dom (h | ( dom B))) = (( dom h) /\ ( dom B)) by RELAT_1: 61

        .= ( NAT /\ ( dom B)) by FUNCT_2:def 1

        .= ( dom B) by XBOOLE_1: 28;

        

         A56: j in ( Seg ( width C)) by A17, A37, ZFMISC_1: 87;

         A57:

        now

          let k9 be object;

          assume

           A58: k9 in ( dom B);

          then

          reconsider k = k9 as Element of NAT ;

          

           A59: k in ( Seg ( width A)) by A1, A58, FINSEQ_1:def 3;

          

           A60: k in ( dom (B * C)) by A1, A3, A58, FINSEQ_3: 29;

          

           A61: [k, j] in ( Indices (B * C)) by A6, A56, A58, ZFMISC_1: 87;

          reconsider p = ( mlt (( Line (B,k)),( Col (C,j)))) as FinSequence of K;

          reconsider a = (A * (i,k)) as Element of K;

          

           A62: ( len ( mlt (( Line (B,k)),( Col (C,j))))) = ( len (the multF of K .: (( Line (B,k)),( Col (C,j))))) by FVSUM_1:def 7;

          ( dom f) = [: NAT , NAT :] by FUNCT_2:def 1;

          then

           A63: ex G be Function st G = (( curry' f) . k) & ( dom G) = NAT & ( rng G) c= ( rng f) & for x st x in NAT holds (G . x) = (f . (x,k)) by FUNCT_5: 32;

          

          then

           A64: ( dom ((( curry' f) . k) | ( dom C))) = ( NAT /\ ( dom C)) by RELAT_1: 61

          .= ( dom C) by XBOOLE_1: 28;

          

           A65: k in ( dom (the multF of K .: (( Line (A,i)),( Col ((B * C),j))))) by A1, A50, A58, FINSEQ_3: 29;

          ( len ( Line (B,k))) = ( len C) by A2, MATRIX_0:def 7

          .= ( len ( Col (C,j))) by MATRIX_0:def 8;

          

          then

           A66: ( len (the multF of K .: (( Line (B,k)),( Col (C,j))))) = ( len ( Line (B,k))) by FINSEQ_2: 72

          .= ( len C) by A2, MATRIX_0:def 7;

          ( dom (a multfield )) = the carrier of K by FUNCT_2:def 1;

          then (a * p) = ((a multfield ) * p) & ( rng p) c= ( dom (a multfield )) by FINSEQ_1:def 4, FVSUM_1:def 6;

          then

           A67: ( dom (a * p)) = ( dom p) by RELAT_1: 27;

          then

           A68: ( dom ((A * (i,k)) * ( mlt (( Line (B,k)),( Col (C,j)))))) = ( dom C) by A62, A66, FINSEQ_3: 29;

           A69:

          now

            let l be object;

            assume

             A70: l in ( dom C);

            then

            reconsider l9 = l as Element of NAT ;

            

             A71: l9 in ( dom (the multF of K .: (( Line (B,k)),( Col (C,j))))) by A66, A70, FINSEQ_3: 29;

            l9 in ( dom p) by A62, A66, A70, FINSEQ_3: 29;

            then

            reconsider b = (p . l9) as Element of K by FINSEQ_2: 11;

            

             A72: l9 in ( Seg ( width B)) by A2, A70, FINSEQ_1:def 3;

            

             A73: l in ( dom (a * p)) by A62, A66, A67, A70, FINSEQ_3: 29;

            

            thus (((( curry' f) . k) | ( dom C)) . l) = ((( curry' f) . k) . l9) by A70, FUNCT_1: 49

            .= (f . (l9,k)) by A63

            .= (((A * (i,k)) * (B * (k,l9))) * (C * (l9,j))) by A19

            .= ((A * (i,k)) * ((B * (k,l9)) * (C * (l9,j)))) by GROUP_1:def 3

            .= (the multF of K . ((A * (i,k)),(the multF of K . ((( Line (B,k)) . l9),(C * (l9,j)))))) by A72, MATRIX_0:def 7

            .= (the multF of K . ((A * (i,k)),(the multF of K . ((( Line (B,k)) . l9),(( Col (C,j)) . l9))))) by A70, MATRIX_0:def 8

            .= (the multF of K . ((A * (i,k)),((the multF of K .: (( Line (B,k)),( Col (C,j)))) . l9))) by A71, FUNCOP_1: 22

            .= (a * b) by FVSUM_1:def 7

            .= (((A * (i,k)) * ( mlt (( Line (B,k)),( Col (C,j))))) . l) by A73, FVSUM_1: 50;

          end;

          (( [#] (((A * (i,k)) * ( mlt (( Line (B,k)),( Col (C,j))))),( 0. K))) | ( dom C)) = ((A * (i,k)) * ( mlt (( Line (B,k)),( Col (C,j))))) by A68, SETWOP_2: 21;

          then

           A74: (( [#] (((A * (i,k)) * ( mlt (( Line (B,k)),( Col (C,j))))),( 0. K))) | ( dom C)) = ((( curry' f) . k) | ( dom C)) by A64, A68, A69, FUNCT_1: 2;

          

          thus ((h | ( dom B)) . k9) = (h . k) by A55, A58, FUNCT_1: 47

          .= (the addF of K $$ (X,(( curry' f) . k))) by A54

          .= (the addF of K $$ (X,( [#] (((A * (i,k)) * ( mlt (( Line (B,k)),( Col (C,j))))),( 0. K))))) by A74, FVSUM_1: 8, SETWOP_2: 7

          .= (the addF of K $$ (a * p)) by A10, A33, A68, SETWOP_2:def 2

          .= ( Sum (a * p)) by FVSUM_1:def 8

          .= ((A * (i,k)) * ( Sum ( mlt (( Line (B,k)),( Col (C,j)))))) by FVSUM_1: 73

          .= ((A * (i,k)) * (( Line (B,k)) "*" ( Col (C,j)))) by FVSUM_1:def 9

          .= ((A * (i,k)) * ((B * C) * (k,j))) by A2, A61, Def4

          .= (the multF of K . ((( Line (A,i)) . k),((B * C) * (k,j)))) by A59, MATRIX_0:def 7

          .= (the multF of K . ((( Line (A,i)) . k),(( Col ((B * C),j)) . k))) by A60, MATRIX_0:def 8

          .= ((the multF of K .: (( Line (A,i)),( Col ((B * C),j)))) . k) by A65, FUNCOP_1: 22

          .= (( mlt (( Line (A,i)),( Col ((B * C),j)))) . k9) by FVSUM_1:def 7;

        end;

        ( dom ( mlt (( Line (A,i)),( Col ((B * C),j))))) = ( dom B) by A1, A50, A51, FINSEQ_3: 29;

        then

         A75: (h | ( dom B)) = ( mlt (( Line (A,i)),( Col ((B * C),j)))) by A55, A57, FUNCT_1: 2;

        ( dom ( mlt (( Line ((A * B),i)),( Col (C,j))))) = ( dom C) by A36, A47, FINSEQ_3: 29;

        then

         A76: (g | ( dom C)) = ( mlt (( Line ((A * B),i)),( Col (C,j)))) by A35, A39, FUNCT_1: 2;

        

        thus (((A * B) * C) * (i,j)) = (( Line ((A * B),i)) "*" ( Col (C,j))) by A11, A37, Def4

        .= ( Sum ( mlt (( Line ((A * B),i)),( Col (C,j))))) by FVSUM_1:def 9

        .= (the addF of K $$ ( mlt (( Line ((A * B),i)),( Col (C,j))))) by FVSUM_1:def 8

        .= (the addF of K $$ (( findom C),( [#] (( mlt (( Line ((A * B),i)),( Col (C,j)))),( 0. K))))) by A10, A33, A48, SETWOP_2:def 2

        .= (the addF of K $$ (X,g)) by A10, A49, A76, SETWOP_2: 7

        .= (the addF of K $$ ( [:X, Y:],f)) by A10, A34, Th30

        .= (the addF of K $$ (Y,h)) by A10, A54, Th32

        .= (the addF of K $$ (( findom ( mlt (( Line (A,i)),( Col ((B * C),j))))),( [#] (( mlt (( Line (A,i)),( Col ((B * C),j)))),( the_unity_wrt the addF of K))))) by A10, A33, A53, A75, A52, SETWOP_2: 7

        .= (the addF of K $$ ( mlt (( Line (A,i)),( Col ((B * C),j))))) by A10, SETWOP_2:def 2

        .= ( Sum ( mlt (( Line (A,i)),( Col ((B * C),j))))) by FVSUM_1:def 8

        .= (( Line (A,i)) "*" ( Col ((B * C),j))) by FVSUM_1:def 9

        .= ((A * (B * C)) * (i,j)) by A3, A9, A18, A37, Def4;

      end;

      hence thesis by A8, A5, A15, A12, MATRIX_0: 21;

    end;

    begin

    definition

      let n, K;

      let M be Matrix of n, K;

      let p be Element of ( Permutations n);

      :: MATRIX_3:def7

      func Path_matrix (p,M) -> FinSequence of K means

      : Def7: ( len it ) = n & for i, j st i in ( dom it ) & j = (p . i) holds (it . i) = (M * (i,j));

      existence

      proof

        defpred P[ Nat, set] means for j st j = (p . $1) holds $2 = (M * ($1,j));

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

        

         A1: for k be Nat st k in ( Seg n1) holds ex x be Element of K st P[k, x]

        proof

          reconsider p as Function of ( Seg n), ( Seg n) by MATRIX_1:def 12;

          let k be Nat;

          assume k in ( Seg n1);

          then (p . k) in ( Seg n) by FUNCT_2: 5;

          then

          reconsider j = (p . k) as Element of NAT ;

          reconsider x = (M * (k,j)) as Element of K;

          take x;

          thus thesis;

        end;

        consider t be FinSequence of K such that

         A2: ( dom t) = ( Seg n1) and

         A3: for k be Nat st k in ( Seg n1) holds P[k, (t . k)] from FINSEQ_1:sch 5( A1);

        take t;

        thus ( len t) = n by A2, FINSEQ_1:def 3;

        let i, j;

        assume i in ( dom t) & j = (p . i);

        hence thesis by A2, A3;

      end;

      uniqueness

      proof

        for p1,p2 be FinSequence of K st (( len p1) = n & for i, j st i in ( dom p1) & j = (p . i) holds (p1 . i) = (M * (i,j))) & (( len p2) = n & for i, j st i in ( dom p2) & j = (p . i) holds (p2 . i) = (M * (i,j))) holds p1 = p2

        proof

          let p1,p2 be FinSequence of K;

          assume that

           A4: ( len p1) = n and

           A5: for i, j st i in ( dom p1) & j = (p . i) holds (p1 . i) = (M * (i,j)) and

           A6: ( len p2) = n and

           A7: for i, j st i in ( dom p2) & j = (p . i) holds (p2 . i) = (M * (i,j));

          

           A8: ( dom p2) = ( Seg n) by A6, FINSEQ_1:def 3;

          

           A9: ( dom p1) = ( Seg n) by A4, FINSEQ_1:def 3;

          for i be Nat st i in ( Seg n) holds (p1 . i) = (p2 . i)

          proof

            reconsider p as Function of ( Seg n), ( Seg n) by MATRIX_1:def 12;

            let i be Nat;

            assume

             A10: i in ( Seg n);

            then (p . i) in ( Seg n) by FUNCT_2: 5;

            then

            reconsider j = (p . i) as Element of NAT ;

            (p1 . i) = (M * (i,j)) by A5, A9, A10;

            hence thesis by A7, A8, A10;

          end;

          hence thesis by A9, A8, FINSEQ_1: 13;

        end;

        hence thesis;

      end;

    end

    definition

      let n;

      let K be Ring;

      let M be Matrix of n, K;

      :: MATRIX_3:def8

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

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

      existence

      proof

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

        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))),p)) and

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

        now

          let p be Element of ( Permutations n);

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

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

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let n;

      let K be Ring;

      let M be Matrix of n, K;

      :: MATRIX_3:def9

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

      coherence ;

    end

    reserve a for Element of K;

    theorem :: MATRIX_3:34

    for K be Ring, a be Element of K holds ( Det <* <*a*>*>) = a

    proof

      let K be Ring, a be Element of K;

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

      

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

      proof

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

        

         A2: ( - (a,p)) = a

        proof

          reconsider q = ( id ( Seg 1)) as Element of ( Permutations 1) by MATRIX_1:def 12;

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

          then q is even by MATRIX_1: 16;

          hence thesis by MATRIX_1:def 16;

        end;

        

         A3: ( len ( Path_matrix (p,M))) = 1 by Def7;

        then

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

        then

         A5: 1 in ( dom ( Path_matrix (p,M))) by FINSEQ_1: 2, TARSKI:def 1;

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

        then (( Path_matrix (p,M)) . 1) = (M * (1,1)) by A5, Def7;

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

        then

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

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

        hence thesis by A6, A2, 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;

    definition

      let n;

      let K;

      let M be Matrix of n, K;

      :: MATRIX_3:def10

      func diagonal_of_Matrix M -> FinSequence of K means ( len it ) = n & for i st i in ( Seg n) holds (it . i) = (M * (i,i));

      existence

      proof

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

        deffunc V( Nat) = (M * ($1,$1));

        consider z be FinSequence of K such that

         A1: ( len z) = n1 & for i be Nat st i in ( dom z) holds (z . i) = V(i) from FINSEQ_2:sch 1;

        take z;

        ( dom z) = ( Seg n1) by A1, FINSEQ_1:def 3;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let p1,p2 be FinSequence of K;

        assume that

         A2: ( len p1) = n and

         A3: for i st i in ( Seg n) holds (p1 . i) = (M * (i,i)) and

         A4: ( len p2) = n and

         A5: for i st i in ( Seg n) holds (p2 . i) = (M * (i,i));

         A6:

        now

          let i be Nat;

          assume

           A7: i in ( Seg n);

          then (p1 . i) = (M * (i,i)) by A3;

          hence (p1 . i) = (p2 . i) by A5, A7;

        end;

        ( dom p1) = ( Seg n) & ( dom p2) = ( Seg n) by A2, A4, FINSEQ_1:def 3;

        hence thesis by A6, FINSEQ_1: 13;

      end;

    end