matrix_4.miz

    begin

    reserve i,j for Nat;

    definition

      let K be Field, M1,M2 be Matrix of K;

      :: MATRIX_4:def1

      func M1 - M2 -> Matrix of K equals (M1 + ( - M2));

      coherence ;

    end

    theorem :: MATRIX_4:1



     Th1: for K be Field, M be Matrix of K holds ( - ( - M)) = M

    proof

      let K be Field, M be Matrix of K;

      per cases by NAT_1: 3;

        suppose

         A1: ( len M) = 0 ;

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

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

        hence thesis by A1, CARD_2: 64;

      end;

        suppose

         A2: ( len M) > 0 ;

        ( len ( - M)) = ( len M) & ( width ( - M)) = ( width M) by MATRIX_3:def 2;

        then

         A3: ( - M) is Matrix of ( len M), ( width M), K by A2, MATRIX_0: 20;

        M is Matrix of ( len M), ( width M), K by A2, MATRIX_0: 20;

        then

         A4: ( Indices ( - M)) = ( Indices M) by A3, MATRIX_0: 26;



         A5: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = (( - ( - M)) * (i,j))

        proof

          let i, j;

          assume

           A6: [i, j] in ( Indices M);

          then (( - M) * (i,j)) = ( - (M * (i,j))) by MATRIX_3:def 2;

          then (( - ( - M)) * (i,j)) = ( - ( - (M * (i,j)))) by A4, A6, MATRIX_3:def 2;

          hence thesis by RLVECT_1: 17;

        end;

        ( width ( - ( - M))) = ( width ( - M)) by MATRIX_3:def 2;

        then

         A7: ( width ( - ( - M))) = ( width M) by MATRIX_3:def 2;

        ( len ( - ( - M))) = ( len ( - M)) by MATRIX_3:def 2;

        then ( len ( - ( - M))) = ( len M) by MATRIX_3:def 2;

        hence thesis by A7, A5, MATRIX_0: 21;

      end;

    end;

    theorem :: MATRIX_4:2



     Th2: for K be Field, M be Matrix of K holds (M + ( - M)) = ( 0. (K,( len M),( width M)))

    proof

      let K be Field, M be Matrix of K;

      per cases by NAT_1: 3;

        suppose ( len M) > 0 ;

        then M is Matrix of ( len M), ( width M), K by MATRIX_0: 20;

        hence thesis by MATRIX_3: 5;

      end;

        suppose

         A1: ( len M) = 0 ;



         A2: ( len (M + ( - M))) = ( len M) by MATRIX_3:def 3;

        ( len ( 0. (K,( len M),( width M)))) = 0 by A1;

        hence thesis by A1, A2, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:3

    for K be Field, M be Matrix of K holds (M - M) = ( 0. (K,( len M),( width M))) by Th2;

    theorem :: MATRIX_4:4

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) & (M1 + M3) = (M2 + M3) holds M1 = M2

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3) and

       A5: (M1 + M3) = (M2 + M3);



       A6: (M3 + ( - M3)) = ( 0. (K,( len M1),( width M1))) by A1, A2, A3, A4, Th2;

      (M1 + (M3 + ( - M3))) = ((M2 + M3) + ( - M3)) by A1, A2, A3, A4, A5, MATRIX_3: 3;

      then

       A7: (M1 + (M3 + ( - M3))) = (M2 + (M3 + ( - M3))) by A2, A4, MATRIX_3: 3;

      per cases by NAT_1: 3;

        suppose

         A8: ( len M1) > 0 ;

        then M2 is Matrix of ( len M1), ( width M1), K by A1, A3, MATRIX_0: 20;

        then

         A9: (M2 + ( 0. (K,( len M1),( width M1)))) = M2 by MATRIX_3: 4;

        M1 is Matrix of ( len M1), ( width M1), K by A8, MATRIX_0: 20;

        hence thesis by A7, A6, A9, MATRIX_3: 4;

      end;

        suppose ( len M1) = 0 ;

        hence thesis by A1, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:5

    for K be Field, M1,M2 be Matrix of K holds (M1 - ( - M2)) = (M1 + M2) by Th1;

    theorem :: MATRIX_4:6

    for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) & M1 = (M1 + M2) holds M2 = ( 0. (K,( len M1),( width M1)))

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( width M1) = ( width M2) and

       A3: M1 = (M1 + M2);

      ( 0. (K,( len M1),( width M1))) = ((M1 + M2) + ( - M1)) by A3, Th2;

      then ( 0. (K,( len M1),( width M1))) = ((M2 + M1) + ( - M1)) by A1, A2, MATRIX_3: 2;

      then ( 0. (K,( len M1),( width M1))) = (M2 + (M1 + ( - M1))) by A1, A2, MATRIX_3: 3;

      then

       A4: ( 0. (K,( len M1),( width M1))) = (M2 + ( 0. (K,( len M1),( width M1)))) by Th2;

      per cases by NAT_1: 3;

        suppose ( len M1) > 0 ;

        then M2 is Matrix of ( len M1), ( width M1), K by A1, A2, MATRIX_0: 20;

        hence thesis by A4, MATRIX_3: 4;

      end;

        suppose

         A5: ( len M1) = 0 ;

        then ( len ( 0. (K,( len M1),( width M1)))) = 0 ;

        hence thesis by A1, A5, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:7



     Th7: for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) & (M1 - M2) = ( 0. (K,( len M1),( width M1))) holds M1 = M2

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( width M1) = ( width M2) and

       A3: (M1 - M2) = ( 0. (K,( len M1),( width M1)));

      per cases by NAT_1: 3;

        suppose

         A4: ( len M1) > 0 ;

        then

         A5: M2 is Matrix of ( len M1), ( width M1), K by A1, A2, MATRIX_0: 20;



         A6: ( len ( - M2)) = ( len M2) & ( width ( - M2)) = ( width M2) by MATRIX_3:def 2;



         A7: ( len ( 0. (K,( len M1),( width M1)))) = ( len M1) by MATRIX_0:def 2;

        then ( width ( 0. (K,( len M1),( width M1)))) = ( width M1) by A4, MATRIX_0: 20;



        then ((M1 + ( - M2)) + M2) = (M2 + ( 0. (K,( len M1),( width M1)))) by A1, A2, A3, A7, MATRIX_3: 2

        .= M2 by A5, MATRIX_3: 4;

        then (M1 + (( - M2) + M2)) = M2 by A1, A2, A6, MATRIX_3: 3;

        then (M1 + (M2 + ( - M2))) = M2 by A6, MATRIX_3: 2;

        then

         A8: (M1 + ( 0. (K,( len M1),( width M1)))) = M2 by A5, MATRIX_3: 5;

        M1 is Matrix of ( len M1), ( width M1), K by A4, MATRIX_0: 20;

        hence thesis by A8, MATRIX_3: 4;

      end;

        suppose ( len M1) = 0 ;

        hence thesis by A1, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:8



     Th8: for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) & (M1 + M2) = ( 0. (K,( len M1),( width M1))) holds M2 = ( - M1)

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2) and

       A2: (M1 + M2) = ( 0. (K,( len M1),( width M1)));



       A3: ( len ( - M2)) = ( len M2) & ( width ( - M2)) = ( width M2) by MATRIX_3:def 2;

      (M1 - ( - M2)) = ( 0. (K,( len M1),( width M1))) by A2, Th1;

      then M1 = ( - M2) by A1, A3, Th7;

      hence thesis by Th1;

    end;

    theorem :: MATRIX_4:9



     Th9: for n,m be Nat, K be Field holds ( - ( 0. (K,n,m))) = ( 0. (K,n,m))

    proof

      let n,m be Nat, K be Field;

      per cases by NAT_1: 3;

        suppose

         A1: n > 0 ;



         A2: (( 0. (K,n,m)) + ( 0. (K,n,m))) = ( 0. (K,n,m)) by MATRIX_3: 4;



         A3: ( len ( 0. (K,n,m))) = n by MATRIX_0:def 2;

        then ( width ( 0. (K,n,m))) = m by A1, MATRIX_0: 20;

        hence thesis by A3, A2, Th8;

      end;

        suppose n = 0 ;

        then

         A4: ( len ( 0. (K,n,m))) = 0 ;

        then ( len ( - ( 0. (K,n,m)))) = 0 by MATRIX_3:def 2;

        hence thesis by A4, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:10

    for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) & (M2 - M1) = M2 holds M1 = ( 0. (K,( len M1),( width M1)))

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2) and

       A2: (M2 - M1) = M2;

      per cases by NAT_1: 3;

        suppose

         A3: ( len M1) > 0 ;



         A4: ( len ( - M1)) = ( len M1) & ( width ( - M1)) = ( width M1) by MATRIX_3:def 2;



         A5: M2 is Matrix of ( len M1), ( width M1), K by A1, A3, MATRIX_0: 20;

        then ((M2 + ( - M1)) + ( - M2)) = ( 0. (K,( len M1),( width M1))) by A2, MATRIX_3: 5;

        then ((( - M1) + M2) + ( - M2)) = ( 0. (K,( len M1),( width M1))) by A1, A4, MATRIX_3: 2;

        then (( - M1) + (M2 + ( - M2))) = ( 0. (K,( len M1),( width M1))) by A1, A4, MATRIX_3: 3;

        then

         A6: (( - M1) + ( 0. (K,( len M1),( width M1)))) = ( 0. (K,( len M1),( width M1))) by A5, MATRIX_3: 5;

        ( - M1) is Matrix of ( len M1), ( width M1), K by A3, A4, MATRIX_0: 20;

        then ( - M1) = ( 0. (K,( len M1),( width M1))) by A6, MATRIX_3: 4;

        then M1 = ( - ( 0. (K,( len M1),( width M1)))) by Th1;

        hence thesis by Th9;

      end;

        suppose

         A7: ( len M1) = 0 ;

        then ( len ( 0. (K,( len M1),( width M1)))) = 0 ;

        hence thesis by A7, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:11



     Th11: for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds M1 = (M1 - (M2 - M2))

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume ( len M1) = ( len M2) & ( width M1) = ( width M2);



      then

       A1: (M1 - (M2 - M2)) = (M1 - ( 0. (K,( len M1),( width M1)))) by Th2

      .= (M1 + ( 0. (K,( len M1),( width M1)))) by Th9;

      per cases by NAT_1: 3;

        suppose ( len M1) > 0 ;

        then M1 is Matrix of ( len M1), ( width M1), K by MATRIX_0: 20;

        hence thesis by A1, MATRIX_3: 4;

      end;

        suppose

         A2: ( len M1) = 0 ;

        then ( len (M1 - (M2 - M2))) = 0 by MATRIX_3:def 3;

        hence thesis by A2, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:12



     Th12: for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds ( - (M1 + M2)) = (( - M1) + ( - M2))

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2);



       A2: ( width ( - M1)) = ( width M1) by MATRIX_3:def 2;

      then

       A3: ( width (( - M1) + ( - M2))) = ( width M1) by MATRIX_3:def 3;



       A4: ( len (M1 + M2)) = ( len M1) & ( width (M1 + M2)) = ( width M1) by MATRIX_3:def 3;



       A5: ( len ( - M1)) = ( len M1) by MATRIX_3:def 2;

      then

       A6: ( len (( - M1) + ( - M2))) = ( len M1) by MATRIX_3:def 3;



       A7: ( len ( - M2)) = ( len M2) & ( width ( - M2)) = ( width M2) by MATRIX_3:def 2;

      per cases by NAT_1: 3;

        suppose

         A8: ( len M1) > 0 ;

        then

         A9: M2 is Matrix of ( len M1), ( width M1), K by A1, MATRIX_0: 20;



         A10: M1 is Matrix of ( len M1), ( width M1), K by A8, MATRIX_0: 20;

        ((M1 + M2) + (( - M1) + ( - M2))) = ((M1 + M2) + (( - M2) + ( - M1))) by A1, A5, A2, A7, MATRIX_3: 2

        .= (((M1 + M2) + ( - M2)) + ( - M1)) by A1, A7, A4, MATRIX_3: 3

        .= ((M1 + (M2 + ( - M2))) + ( - M1)) by A1, MATRIX_3: 3

        .= ((M1 + ( 0. (K,( len M1),( width M1)))) + ( - M1)) by A9, MATRIX_3: 5

        .= (M1 + ( - M1)) by A10, MATRIX_3: 4

        .= ( 0. (K,( len M1),( width M1))) by A10, MATRIX_3: 5;

        hence thesis by A4, A6, A3, Th8;

      end;

        suppose

         A11: ( len M1) = 0 ;

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

        then

         A12: ( len (( - M1) + ( - M2))) = 0 by MATRIX_3:def 3;

        ( len (M1 + M2)) = 0 by A11, MATRIX_3:def 3;

        then ( len ( - (M1 + M2))) = 0 by MATRIX_3:def 2;

        hence thesis by A12, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:13

    for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds (M1 - (M1 - M2)) = M2

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( width M1) = ( width M2);



       A3: ( len ( - M1)) = ( len M1) & ( width ( - M1)) = ( width M1) by MATRIX_3:def 2;



       A4: ( len ( - M2)) = ( len M2) & ( width ( - M2)) = ( width M2) by MATRIX_3:def 2;

      per cases by NAT_1: 3;

        suppose

         A5: ( len M1) > 0 ;



         A6: ( len ( 0. (K,( len M1),( width M1)))) = ( len M1) by MATRIX_0:def 2;

        then

         A7: ( width ( 0. (K,( len M1),( width M1)))) = ( width M1) by A5, MATRIX_0: 20;



         A8: M2 is Matrix of ( len M1), ( width M1), K by A1, A2, A5, MATRIX_0: 20;



         A9: M1 is Matrix of ( len M1), ( width M1), K by A5, MATRIX_0: 20;

        (M1 - (M1 - M2)) = (M1 + (( - M1) + ( - ( - M2)))) by A1, A2, A4, Th12

        .= (M1 + (( - M1) + M2)) by Th1

        .= ((M1 + ( - M1)) + M2) by A3, MATRIX_3: 3

        .= (( 0. (K,( len M1),( width M1))) + M2) by A9, MATRIX_3: 5

        .= (M2 + ( 0. (K,( len M1),( width M1)))) by A1, A2, A6, A7, MATRIX_3: 2

        .= M2 by A8, MATRIX_3: 4;

        hence thesis;

      end;

        suppose

         A10: ( len M1) = 0 ;

        then ( len (M1 - (M1 - M2))) = 0 by MATRIX_3:def 3;

        hence thesis by A1, A10, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:14



     Th14: for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) & (M1 - M3) = (M2 - M3) holds M1 = M2

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3) and

       A5: (M1 - M3) = (M2 - M3);



       A6: ( len ( - M3)) = ( len M3) & ( width ( - M3)) = ( width M3) by MATRIX_3:def 2;

      per cases by NAT_1: 3;

        suppose

         A7: ( len M1) > 0 ;

        then

         A8: M2 is Matrix of ( len M1), ( width M1), K by A1, A3, MATRIX_0: 20;



         A9: M3 is Matrix of ( len M1), ( width M1), K by A1, A2, A3, A4, A7, MATRIX_0: 20;

        ((M1 + ( - M3)) + M3) = (M2 + (( - M3) + M3)) by A2, A4, A5, A6, MATRIX_3: 3;

        then ((M1 + ( - M3)) + M3) = (M2 + (M3 + ( - M3))) by A6, MATRIX_3: 2;

        then ((M1 + ( - M3)) + M3) = (M2 + ( 0. (K,( len M1),( width M1)))) by A9, MATRIX_3: 5;

        then ((M1 + ( - M3)) + M3) = M2 by A8, MATRIX_3: 4;

        then (M1 + (( - M3) + M3)) = M2 by A1, A2, A3, A4, A6, MATRIX_3: 3;

        then (M1 + (M3 + ( - M3))) = M2 by A6, MATRIX_3: 2;

        then

         A10: (M1 + ( 0. (K,( len M1),( width M1)))) = M2 by A9, MATRIX_3: 5;

        M1 is Matrix of ( len M1), ( width M1), K by A7, MATRIX_0: 20;

        hence thesis by A10, MATRIX_3: 4;

      end;

        suppose ( len M1) = 0 ;

        hence thesis by A1, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:15



     Th15: for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) & (M3 - M1) = (M3 - M2) holds M1 = M2

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3) and

       A5: (M3 - M1) = (M3 - M2);

      per cases by NAT_1: 3;

        suppose

         A6: ( len M1) > 0 ;

        then

         A7: M3 is Matrix of ( len M1), ( width M1), K by A1, A2, A3, A4, MATRIX_0: 20;



         A8: ( len ( - M2)) = ( len M2) & ( width ( - M2)) = ( width M2) by MATRIX_3:def 2;

        then

         A9: ( - M2) is Matrix of ( len M1), ( width M1), K by A1, A3, A6, MATRIX_0: 20;



         A10: ( len ( - M1)) = ( len M1) & ( width ( - M1)) = ( width M1) by MATRIX_3:def 2;

        then (( - M1) + M3) = (M3 + ( - M2)) by A1, A2, A3, A4, A5, MATRIX_3: 2;

        then (( - M1) + M3) = (( - M2) + M3) by A2, A4, A8, MATRIX_3: 2;

        then ((( - M1) + M3) + ( - M3)) = (( - M2) + (M3 + ( - M3))) by A2, A4, A8, MATRIX_3: 3;

        then ((( - M1) + M3) + ( - M3)) = (( - M2) + ( 0. (K,( len M1),( width M1)))) by A7, MATRIX_3: 5;

        then ((( - M1) + M3) + ( - M3)) = ( - M2) by A9, MATRIX_3: 4;

        then (( - M1) + (M3 + ( - M3))) = ( - M2) by A1, A2, A3, A4, A10, MATRIX_3: 3;

        then

         A11: (( - M1) + ( 0. (K,( len M1),( width M1)))) = ( - M2) by A7, MATRIX_3: 5;

        ( - M1) is Matrix of ( len M1), ( width M1), K by A6, A10, MATRIX_0: 20;

        then ( - M1) = ( - M2) by A11, MATRIX_3: 4;

        then ( - ( - M1)) = M2 by Th1;

        hence thesis by Th1;

      end;

        suppose ( len M1) = 0 ;

        hence thesis by A1, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:16



     Th16: for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds ((M1 - M2) - M3) = ((M1 - M3) - M2)

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);



       A5: ( len ( - M3)) = ( len M3) & ( width ( - M3)) = ( width M3) by MATRIX_3:def 2;



       A6: ( len ( - M2)) = ( len M2) & ( width ( - M2)) = ( width M2) by MATRIX_3:def 2;



      hence ((M1 - M2) - M3) = (M1 + (( - M2) + ( - M3))) by A1, A3, MATRIX_3: 3

      .= (M1 + (( - M3) + ( - M2))) by A2, A4, A6, A5, MATRIX_3: 2

      .= ((M1 - M3) - M2) by A1, A2, A3, A4, A5, MATRIX_3: 3;

    end;

    theorem :: MATRIX_4:17

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds (M1 - M3) = ((M1 - M2) - (M3 - M2))

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);



       A5: ( len ( - M2)) = ( len M2) & ( width ( - M2)) = ( width M2) by MATRIX_3:def 2;



       A6: ( len ( - M3)) = ( len M3) & ( width ( - M3)) = ( width M3) by MATRIX_3:def 2;

      per cases by NAT_1: 3;

        suppose

         A7: ( len M1) > 0 ;

        then

         A8: M2 is Matrix of ( len M1), ( width M1), K by A1, A3, MATRIX_0: 20;



         A9: ( len (M1 + ( - M2))) = ( len M1) & ( width (M1 + ( - M2))) = ( width M1) by MATRIX_3:def 3;



         A10: M1 is Matrix of ( len M1), ( width M1), K by A7, MATRIX_0: 20;

        ((M1 - M2) - (M3 - M2)) = ((M1 + ( - M2)) + (( - M3) + ( - ( - M2)))) by A2, A4, A5, Th12

        .= ((M1 + ( - M2)) + (( - M3) + M2)) by Th1

        .= ((M1 + ( - M2)) + (M2 + ( - M3))) by A2, A4, A6, MATRIX_3: 2

        .= (((M1 + ( - M2)) + M2) + ( - M3)) by A1, A3, A9, MATRIX_3: 3

        .= ((M1 + (( - M2) + M2)) + ( - M3)) by A1, A3, A5, MATRIX_3: 3

        .= ((M1 + (M2 + ( - M2))) + ( - M3)) by A5, MATRIX_3: 2

        .= ((M1 + ( 0. (K,( len M1),( width M1)))) + ( - M3)) by A8, MATRIX_3: 5

        .= (M1 + ( - M3)) by A10, MATRIX_3: 4;

        hence thesis;

      end;

        suppose

         A11: ( len M1) = 0 ;

        then ( len (M1 - M2)) = 0 by MATRIX_3:def 3;

        then

         A12: ( len ((M1 - M2) - (M3 - M2))) = 0 by MATRIX_3:def 3;

        ( len (M1 - M3)) = 0 by A11, MATRIX_3:def 3;

        hence thesis by A12, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:18



     Th18: for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds ((M3 - M1) - (M3 - M2)) = (M2 - M1)

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);

      per cases by NAT_1: 3;

        suppose

         A5: ( len M1) > 0 ;

        then

         A6: M3 is Matrix of ( len M1), ( width M1), K by A1, A2, A3, A4, MATRIX_0: 20;



         A7: ( len ( - M2)) = ( len M2) & ( width ( - M2)) = ( width M2) by MATRIX_3:def 2;



         A8: ( width ( - M1)) = ( width M1) by MATRIX_3:def 2;

        then

         A9: ( width (( - M1) + M3)) = ( width M1) by MATRIX_3:def 3;



         A10: ( len ( - M3)) = ( len M3) & ( width ( - M3)) = ( width M3) by MATRIX_3:def 2;



         A11: ( len ( - M1)) = ( len M1) by MATRIX_3:def 2;

        then

         A12: ( len (( - M1) + M3)) = ( len M1) by MATRIX_3:def 3;



         A13: ( - M1) is Matrix of ( len M1), ( width M1), K by A5, A11, A8, MATRIX_0: 20;

        ((M3 - M1) - (M3 - M2)) = ((( - M1) + M3) - (M3 + ( - M2))) by A1, A2, A3, A4, A11, A8, MATRIX_3: 2

        .= ((( - M1) + M3) + (( - M3) + ( - ( - M2)))) by A2, A4, A7, Th12

        .= ((( - M1) + M3) + (( - M3) + M2)) by Th1

        .= (((( - M1) + M3) + ( - M3)) + M2) by A1, A2, A3, A4, A10, A12, A9, MATRIX_3: 3

        .= ((( - M1) + (M3 + ( - M3))) + M2) by A1, A2, A3, A4, A11, A8, MATRIX_3: 3

        .= ((( - M1) + ( 0. (K,( len M1),( width M1)))) + M2) by A6, MATRIX_3: 5

        .= (( - M1) + M2) by A13, MATRIX_3: 4

        .= (M2 + ( - M1)) by A1, A3, A11, A8, MATRIX_3: 2;

        hence thesis;

      end;

        suppose

         A14: ( len M1) = 0 ;



         A15: ( len (M2 - M1)) = ( len M2) by MATRIX_3:def 3;

        ( len ((M3 - M1) - (M3 - M2))) = ( len (M3 - M1)) by MATRIX_3:def 3

        .= ( len M3) by MATRIX_3:def 3;

        hence thesis by A1, A2, A14, A15, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:19

    for K be Field, M1,M2,M3,M4 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( len M3) = ( len M4) & ( width M1) = ( width M2) & ( width M2) = ( width M3) & ( width M3) = ( width M4) & (M1 - M2) = (M3 - M4) holds (M1 - M3) = (M2 - M4)

    proof

      let K be Field, M1,M2,M3,M4 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( len M3) = ( len M4) and

       A4: ( width M1) = ( width M2) and

       A5: ( width M2) = ( width M3) and

       A6: ( width M3) = ( width M4) and

       A7: (M1 - M2) = (M3 - M4);



       A8: ( len ( - M4)) = ( len M1) & ( width ( - M4)) = ( width M1) by A1, A2, A3, A4, A5, A6, MATRIX_3:def 2;



       A9: ( len (M3 + ( - M4))) = ( len M1) & ( width (M3 + ( - M4))) = ( width M1) by A1, A2, A4, A5, MATRIX_3:def 3;



       A10: ( len ( - M2)) = ( len M2) & ( width ( - M2)) = ( width M2) by MATRIX_3:def 2;



       A11: ( len (M1 + ( - M3))) = ( len M1) & ( width (M1 + ( - M3))) = ( width M1) by MATRIX_3:def 3;



       A12: ( len (M1 + ( - M2))) = ( len M1) & ( width (M1 + ( - M2))) = ( width M1) by MATRIX_3:def 3;



       A13: ( len (M1 + ( - M3))) = ( len M1) & ( width (M1 + ( - M3))) = ( width M1) by MATRIX_3:def 3;



       A14: ( len (M2 + ( - M4))) = ( len M1) & ( width (M2 + ( - M4))) = ( width M1) by A1, A4, MATRIX_3:def 3;



       A15: ( len ( - M3)) = ( len M3) & ( width ( - M3)) = ( width M3) by MATRIX_3:def 2;

      per cases by NAT_1: 3;

        suppose ( len M1) > 0 ;

        then (M3 + ( - M4)) is Matrix of ( len M1), ( width M1), K by A9, MATRIX_0: 20;

        then ((M1 + ( - M2)) + ( - (M3 + ( - M4)))) = ( 0. (K,( len M1),( width M1))) by A7, MATRIX_3: 5;

        then ((M1 + ( - M2)) + (( - M3) + ( - ( - M4)))) = ( 0. (K,( len M1),( width M1))) by A1, A2, A4, A5, A8, Th12;

        then ((M1 + ( - M2)) + (( - M3) + M4)) = ( 0. (K,( len M1),( width M1))) by Th1;

        then (((M1 + ( - M2)) + ( - M3)) + M4) = ( 0. (K,( len M1),( width M1))) by A1, A2, A4, A5, A15, A12, MATRIX_3: 3;

        then ((M1 + (( - M2) + ( - M3))) + M4) = ( 0. (K,( len M1),( width M1))) by A1, A4, A10, MATRIX_3: 3;

        then ((M1 + (( - M3) + ( - M2))) + M4) = ( 0. (K,( len M1),( width M1))) by A2, A5, A10, A15, MATRIX_3: 2;

        then (((M1 + ( - M3)) + ( - M2)) + M4) = ( 0. (K,( len M1),( width M1))) by A1, A2, A4, A5, A15, MATRIX_3: 3;

        then ((M1 + ( - M3)) + (( - M2) + M4)) = ( 0. (K,( len M1),( width M1))) by A1, A4, A10, A11, MATRIX_3: 3;

        then ((M1 + ( - M3)) + (( - M2) + ( - ( - M4)))) = ( 0. (K,( len M1),( width M1))) by Th1;

        then ((M1 + ( - M3)) - (M2 + ( - M4))) = ( 0. (K,( len M1),( width M1))) by A1, A4, A8, Th12;

        hence thesis by A13, A14, Th7;

      end;

        suppose ( len M1) = 0 ;

        then ( len (M1 - M3)) = 0 & ( len (M2 - M4)) = 0 by A1, MATRIX_3:def 3;

        hence thesis by CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:20



     Th20: for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds M1 = (M1 + (M2 - M2))

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2);

      per cases by NAT_1: 3;

        suppose

         A2: ( len M1) > 0 ;

        then

         A3: M1 is Matrix of ( len M1), ( width M1), K by MATRIX_0: 20;

        M2 is Matrix of ( len M1), ( width M1), K by A1, A2, MATRIX_0: 20;



        hence (M1 + (M2 - M2)) = (M1 + ( 0. (K,( len M1),( width M1)))) by MATRIX_3: 5

        .= M1 by A3, MATRIX_3: 4;

      end;

        suppose

         A4: ( len M1) = 0 ;

        ( len (M1 + (M2 - M2))) = ( len M1) by MATRIX_3:def 3;

        hence thesis by A4, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:21



     Th21: for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds M1 = ((M1 + M2) - M2)

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2);



      hence ((M1 + M2) - M2) = (M1 + (M2 - M2)) by MATRIX_3: 3

      .= M1 by A1, Th20;

    end;

    theorem :: MATRIX_4:22



     Th22: for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds M1 = ((M1 - M2) + M2)

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2);

      then

       A2: ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by MATRIX_3:def 2;



      hence ((M1 - M2) + M2) = (M1 + (( - M2) + M2)) by MATRIX_3: 3

      .= (M1 + (M2 - M2)) by A1, A2, MATRIX_3: 2

      .= M1 by A1, Th20;

    end;

    theorem :: MATRIX_4:23

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds (M1 + M3) = ((M1 + M2) + (M3 - M2))

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);



       A5: ( len (M1 + M2)) = ( len M1) & ( width (M1 + M2)) = ( width M1) by MATRIX_3:def 3;



       A6: ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by A1, A3, MATRIX_3:def 2;



      hence ((M1 + M2) + (M3 - M2)) = ((M1 + M2) + (( - M2) + M3)) by A1, A2, A3, A4, MATRIX_3: 2

      .= (((M1 + M2) + ( - M2)) + M3) by A6, A5, MATRIX_3: 3

      .= ((M1 + (M2 - M2)) + M3) by A1, A3, MATRIX_3: 3

      .= (M1 + M3) by A1, A3, Th20;

    end;

    theorem :: MATRIX_4:24

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds ((M1 + M2) - M3) = ((M1 - M3) + M2)

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);



       A5: ( len ( - M3)) = ( len M1) & ( width ( - M3)) = ( width M1) by A1, A2, A3, A4, MATRIX_3:def 2;



      thus ((M1 + M2) - M3) = (M1 + (M2 + ( - M3))) by A1, A3, MATRIX_3: 3

      .= (M1 + (( - M3) + M2)) by A1, A3, A5, MATRIX_3: 2

      .= ((M1 - M3) + M2) by A5, MATRIX_3: 3;

    end;

    theorem :: MATRIX_4:25

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds ((M1 - M2) + M3) = ((M3 - M2) + M1)

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);



       A5: ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by A1, A3, MATRIX_3:def 2;



      hence ((M1 - M2) + M3) = ((( - M2) + M1) + M3) by MATRIX_3: 2

      .= (( - M2) + (M1 + M3)) by A5, MATRIX_3: 3

      .= (( - M2) + (M3 + M1)) by A1, A2, A3, A4, MATRIX_3: 2

      .= ((( - M2) + M3) + M1) by A1, A2, A3, A4, A5, MATRIX_3: 3

      .= ((M3 - M2) + M1) by A1, A2, A3, A4, A5, MATRIX_3: 2;

    end;

    theorem :: MATRIX_4:26



     Th26: for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds (M1 + M3) = ((M1 + M2) - (M2 - M3))

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);

      per cases by NAT_1: 3;

        suppose

         A5: ( len M1) > 0 ;

        then

         A6: M2 is Matrix of ( len M1), ( width M1), K by A1, A3, MATRIX_0: 20;



         A7: ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by A1, A3, MATRIX_3:def 2;



         A8: ( len ( - M3)) = ( len M1) & ( width ( - M3)) = ( width M1) by A1, A2, A3, A4, MATRIX_3:def 2;



         A9: ( len (M1 + M2)) = ( len M1) & ( width (M1 + M2)) = ( width M1) by MATRIX_3:def 3;

        M1 is Matrix of ( len M1), ( width M1), K by A5, MATRIX_0: 20;



        hence (M1 + M3) = ((M1 + ( 0. (K,( len M1),( width M1)))) + M3) by MATRIX_3: 4

        .= ((M1 + (M2 + ( - M2))) + M3) by A6, MATRIX_3: 5

        .= (((M1 + M2) + ( - M2)) + M3) by A1, A3, MATRIX_3: 3

        .= ((M1 + M2) + (( - M2) + M3)) by A7, A9, MATRIX_3: 3

        .= ((M1 + M2) + (( - M2) + ( - ( - M3)))) by Th1

        .= ((M1 + M2) - (M2 - M3)) by A1, A3, A8, Th12;

      end;

        suppose

         A10: ( len M1) = 0 ;



         A11: ( len ((M1 + M2) - (M2 - M3))) = ( len (M1 + M2)) by MATRIX_3:def 3

        .= ( len M1) by MATRIX_3:def 3;

        ( len (M1 + M3)) = ( len M1) by MATRIX_3:def 3;

        hence thesis by A10, A11, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:27

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds (M1 - M3) = ((M1 + M2) - (M3 + M2))

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);

      ( len ( - M3)) = ( len M1) & ( width ( - M3)) = ( width M1) by A1, A2, A3, A4, MATRIX_3:def 2;



      hence (M1 - M3) = ((M1 + M2) - (M2 - ( - M3))) by A1, A3, Th26

      .= ((M1 + M2) - (M2 + M3)) by Th1

      .= ((M1 + M2) - (M3 + M2)) by A2, A4, MATRIX_3: 2;

    end;

    theorem :: MATRIX_4:28



     Th28: for K be Field, M1,M2,M3,M4 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( len M3) = ( len M4) & ( width M1) = ( width M2) & ( width M2) = ( width M3) & ( width M3) = ( width M4) & (M1 + M2) = (M3 + M4) holds (M1 - M3) = (M4 - M2)

    proof

      let K be Field, M1,M2,M3,M4 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( len M3) = ( len M4) and

       A4: ( width M1) = ( width M2) and

       A5: ( width M2) = ( width M3) and

       A6: ( width M3) = ( width M4) and

       A7: (M1 + M2) = (M3 + M4);



       A8: ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by A1, A4, MATRIX_3:def 2;

      (M1 + M2) = (M4 + M3) by A3, A6, A7, MATRIX_3: 2;

      then ((M1 + M2) + ( - M2)) = (M4 + (M3 + ( - M2))) by A3, A6, MATRIX_3: 3;

      then ((M1 + M2) + ( - M2)) = (M4 + (( - M2) + M3)) by A1, A2, A4, A5, A8, MATRIX_3: 2;

      then (M1 + (M2 - M2)) = (M4 + (( - M2) + M3)) by A1, A4, MATRIX_3: 3;

      then M1 = (M4 + (( - M2) + M3)) by A1, A4, Th20;

      then

       A9: M1 = ((M4 + ( - M2)) + M3) by A1, A2, A3, A4, A5, A6, A8, MATRIX_3: 3;

      ( len (M4 + ( - M2))) = ( len M1) & ( width (M4 + ( - M2))) = ( width M1) by A1, A2, A3, A4, A5, A6, MATRIX_3:def 3;

      hence thesis by A1, A2, A4, A5, A9, Th21;

    end;

    theorem :: MATRIX_4:29

    for K be Field, M1,M2,M3,M4 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( len M3) = ( len M4) & ( width M1) = ( width M2) & ( width M2) = ( width M3) & ( width M3) = ( width M4) & (M1 - M3) = (M4 - M2) holds (M1 + M2) = (M3 + M4)

    proof

      let K be Field, M1,M2,M3,M4 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( len M3) = ( len M4) and

       A4: ( width M1) = ( width M2) and

       A5: ( width M2) = ( width M3) and

       A6: ( width M3) = ( width M4) and

       A7: (M1 - M3) = (M4 - M2);



       A8: ( len ( - M3)) = ( len M1) & ( width ( - M3)) = ( width M1) by A1, A2, A4, A5, MATRIX_3:def 2;



       A9: ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by A1, A4, MATRIX_3:def 2;

      then (M1 + ( - M3)) = (( - M2) + M4) by A1, A2, A3, A4, A5, A6, A7, MATRIX_3: 2;

      then (M1 - ( - M2)) = (M4 - ( - M3)) by A1, A2, A3, A4, A5, A6, A9, A8, Th28;

      then (M1 + M2) = (M4 - ( - M3)) by Th1;

      then (M1 + M2) = (M4 + M3) by Th1;

      hence thesis by A3, A6, MATRIX_3: 2;

    end;

    theorem :: MATRIX_4:30

    for K be Field, M1,M2,M3,M4 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( len M3) = ( len M4) & ( width M1) = ( width M2) & ( width M2) = ( width M3) & ( width M3) = ( width M4) & (M1 + M2) = (M3 - M4) holds (M1 + M4) = (M3 - M2)

    proof

      let K be Field, M1,M2,M3,M4 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) & ( len M2) = ( len M3) and

       A2: ( len M3) = ( len M4) and

       A3: ( width M1) = ( width M2) & ( width M2) = ( width M3) and

       A4: ( width M3) = ( width M4) and

       A5: (M1 + M2) = (M3 - M4);



       A6: ( len ( - M4)) = ( len M1) & ( width ( - M4)) = ( width M1) by A1, A2, A3, A4, MATRIX_3:def 2;

      then (M1 + M2) = (( - M4) + M3) by A1, A3, A5, MATRIX_3: 2;

      then (M1 - ( - M4)) = (M3 - M2) by A1, A3, A6, Th28;

      hence thesis by Th1;

    end;

    theorem :: MATRIX_4:31



     Th31: for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds (M1 - (M2 + M3)) = ((M1 - M2) - M3)

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);



       A5: ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by A1, A3, MATRIX_3:def 2;

      (M1 - (M2 + M3)) = (M1 + (( - M2) + ( - M3))) by A2, A4, Th12

      .= ((M1 - M2) + ( - M3)) by A5, MATRIX_3: 3;

      hence thesis;

    end;

    theorem :: MATRIX_4:32

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds (M1 - (M2 - M3)) = ((M1 - M2) + M3)

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);

      ( len ( - M3)) = ( len M1) & ( width ( - M3)) = ( width M1) by A1, A2, A3, A4, MATRIX_3:def 2;



      then (M1 - (M2 - M3)) = ((M1 - M2) - ( - M3)) by A1, A3, Th31

      .= ((M1 + ( - M2)) + M3) by Th1;

      hence thesis;

    end;

    theorem :: MATRIX_4:33

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds (M1 - (M2 - M3)) = (M1 + (M3 - M2))

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);



       A5: ( len ( - M3)) = ( len M1) & ( width ( - M3)) = ( width M1) by A1, A2, A3, A4, MATRIX_3:def 2;



      then (M1 - (M2 - M3)) = (M1 + ( - (( - M3) + M2))) by A1, A3, MATRIX_3: 2

      .= (M1 + (( - ( - M3)) + ( - M2))) by A1, A3, A5, Th12

      .= (M1 + (M3 + ( - M2))) by Th1;

      hence thesis;

    end;

    theorem :: MATRIX_4:34

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds (M1 - M3) = ((M1 - M2) + (M2 - M3))

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2);

      then

       A2: ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by MATRIX_3:def 2;

      ( len (M1 + ( - M2))) = ( len M1) & ( width (M1 + ( - M2))) = ( width M1) by MATRIX_3:def 3;



      then ((M1 - M2) + (M2 - M3)) = (((M1 + ( - M2)) + M2) + ( - M3)) by A1, MATRIX_3: 3

      .= ((M1 + (( - M2) + M2)) + ( - M3)) by A2, MATRIX_3: 3

      .= ((M1 + (M2 - M2)) + ( - M3)) by A1, A2, MATRIX_3: 2

      .= (M1 + ( - M3)) by A1, Th20;

      hence thesis;

    end;

    theorem :: MATRIX_4:35

    for K be Field, M1,M2,M3 be Matrix of K st ( - M1) = ( - M2) holds M1 = M2

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume ( - M1) = ( - M2);

      then ( - ( - M1)) = M2 by Th1;

      hence thesis by Th1;

    end;

    theorem :: MATRIX_4:36

    for K be Field, M be Matrix of K st ( - M) = ( 0. (K,( len M),( width M))) holds M = ( 0. (K,( len M),( width M)))

    proof

      let K be Field, M be Matrix of K;

      assume ( - M) = ( 0. (K,( len M),( width M)));

      then ( - ( - M)) = ( 0. (K,( len M),( width M))) by Th9;

      hence thesis by Th1;

    end;

    theorem :: MATRIX_4:37

    for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) & (M1 + ( - M2)) = ( 0. (K,( len M1),( width M1))) holds M1 = M2

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2) and

       A2: (M1 + ( - M2)) = ( 0. (K,( len M1),( width M1)));

      (M1 - M2) = ( 0. (K,( len M1),( width M1))) by A2;

      hence thesis by A1, Th7;

    end;

    theorem :: MATRIX_4:38



     Th38: for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds M1 = ((M1 + M2) + ( - M2))

    proof

      let K be Field, M1,M2 be Matrix of K;



       A1: ((M1 + M2) + ( - M2)) = ((M1 + M2) - M2);

      assume ( len M1) = ( len M2) & ( width M1) = ( width M2);

      hence thesis by A1, Th21;

    end;

    theorem :: MATRIX_4:39

    for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds M1 = (M1 + (M2 + ( - M2)))

    proof

      let K be Field, M1,M2 be Matrix of K;



       A1: (M1 + (M2 + ( - M2))) = (M1 + (M2 - M2));

      assume ( len M1) = ( len M2) & ( width M1) = ( width M2);

      hence thesis by A1, Th20;

    end;

    theorem :: MATRIX_4:40

    for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds M1 = ((( - M2) + M1) + M2)

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume

       A1: ( len M1) = ( len M2) & ( width M1) = ( width M2);

      then ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by MATRIX_3:def 2;

      then ((( - M2) + M1) + M2) = ((M1 - M2) + M2) by MATRIX_3: 2;

      hence thesis by A1, Th22;

    end;

    theorem :: MATRIX_4:41

    for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds ( - (( - M1) + M2)) = (M1 + ( - M2))

    proof

      let K be Field, M1,M2 be Matrix of K;



       A1: ( len ( - M1)) = ( len M1) & ( width ( - M1)) = ( width M1) by MATRIX_3:def 2;

      assume ( len M1) = ( len M2) & ( width M1) = ( width M2);

      then ( - (( - M1) + M2)) = (( - ( - M1)) + ( - M2)) by A1, Th12;

      hence thesis by Th1;

    end;

    theorem :: MATRIX_4:42

    for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds (M1 + M2) = ( - (( - M1) + ( - M2)))

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume ( len M1) = ( len M2) & ( width M1) = ( width M2);

      then

       A1: ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by MATRIX_3:def 2;

      ( len ( - M1)) = ( len M1) & ( width ( - M1)) = ( width M1) by MATRIX_3:def 2;



      then ( - (( - M1) + ( - M2))) = (( - ( - M1)) + ( - ( - M2))) by A1, Th12

      .= (M1 + ( - ( - M2))) by Th1;

      hence thesis by Th1;

    end;

    theorem :: MATRIX_4:43

    for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds ( - (M1 - M2)) = (M2 - M1)

    proof

      let K be Field, M1,M2 be Matrix of K;



       A1: ( len ( - M1)) = ( len M1) & ( width ( - M1)) = ( width M1) by MATRIX_3:def 2;

      assume

       A2: ( len M1) = ( len M2) & ( width M1) = ( width M2);

      then ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by MATRIX_3:def 2;



      then ( - (M1 - M2)) = (( - M1) + ( - ( - M2))) by Th12

      .= (( - M1) + M2) by Th1

      .= (M2 + ( - M1)) by A2, A1, MATRIX_3: 2;

      hence thesis;

    end;

    theorem :: MATRIX_4:44



     Th44: for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds (( - M1) - M2) = (( - M2) - M1)

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume ( len M1) = ( len M2) & ( width M1) = ( width M2);

      then

       A1: ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by MATRIX_3:def 2;

      ( len ( - M1)) = ( len M1) & ( width ( - M1)) = ( width M1) by MATRIX_3:def 2;

      hence thesis by A1, MATRIX_3: 2;

    end;

    theorem :: MATRIX_4:45

    for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds M1 = (( - M2) - (( - M1) - M2))

    proof

      let K be Field, M1,M2 be Matrix of K;



       A1: ( len (M1 + M2)) = ( len M1) & ( width (M1 + M2)) = ( width M1) by MATRIX_3:def 3;

      assume

       A2: ( len M1) = ( len M2) & ( width M1) = ( width M2);

      then

       A3: ( len ( - M2)) = ( len M1) & ( width ( - M2)) = ( width M1) by MATRIX_3:def 2;

      ( len ( - M1)) = ( len M1) & ( width ( - M1)) = ( width M1) by MATRIX_3:def 2;



      then (( - M2) - (( - M1) - M2)) = (( - M2) + (( - ( - M1)) + ( - ( - M2)))) by A3, Th12

      .= (( - M2) + (M1 + ( - ( - M2)))) by Th1

      .= (( - M2) + (M1 + M2)) by Th1

      .= ((M1 + M2) + ( - M2)) by A3, A1, MATRIX_3: 2;

      hence thesis by A2, Th38;

    end;

    theorem :: MATRIX_4:46



     Th46: for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds ((( - M1) - M2) - M3) = ((( - M1) - M3) - M2)

    proof

      let K be Field, M1,M2,M3 be Matrix of K;



       A1: ( len ( - M1)) = ( len M1) & ( width ( - M1)) = ( width M1) by MATRIX_3:def 2;

      assume ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3);

      hence thesis by A1, Th16;

    end;

    theorem :: MATRIX_4:47



     Th47: for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds ((( - M1) - M2) - M3) = ((( - M2) - M3) - M1)

    proof

      let K be Field, M1,M2,M3 be Matrix of K such that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);

      ((( - M1) - M2) - M3) = ((( - M2) - M1) - M3) by A1, A3, Th44;

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

    end;

    theorem :: MATRIX_4:48

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds ((( - M1) - M2) - M3) = ((( - M3) - M2) - M1)

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume

       A1: ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3);

      then ((( - M1) - M2) - M3) = ((( - M1) - M3) - M2) by Th46;

      hence thesis by A1, Th47;

    end;

    theorem :: MATRIX_4:49

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) holds ((M3 - M1) - (M3 - M2)) = ( - (M1 - M2))

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( len M2) = ( len M3) and

       A3: ( width M1) = ( width M2) and

       A4: ( width M2) = ( width M3);



       A5: ( len ( - M1)) = ( len M1) & ( width ( - M1)) = ( width M1) by MATRIX_3:def 2;



       A6: ( len ( - M2)) = ( len M2) & ( width ( - M2)) = ( width M2) by MATRIX_3:def 2;

      ((M3 - M1) - (M3 - M2)) = (M2 - M1) by A1, A2, A3, A4, Th18

      .= (( - M1) + M2) by A1, A3, A5, MATRIX_3: 2

      .= (( - M1) + ( - ( - M2))) by Th1

      .= ( - (M1 + ( - M2))) by A1, A3, A6, Th12;

      hence thesis;

    end;

    theorem :: MATRIX_4:50

    for K be Field, M be Matrix of K holds (( 0. (K,( len M),( width M))) - M) = ( - M)

    proof

      let K be Field, M be Matrix of K;



       A1: ( len ( - M)) = ( len M) by MATRIX_3:def 2;



       A2: ( width ( - M)) = ( width M) by MATRIX_3:def 2;



       A3: ( len ( 0. (K,( len M),( width M)))) = ( len M) by MATRIX_0:def 2;

      per cases by NAT_1: 3;

        suppose

         A4: ( len M) > 0 ;

        then ( width ( 0. (K,( len M),( width M)))) = ( width M) by A3, MATRIX_0: 20;

        then

         A5: (( 0. (K,( len M),( width M))) - M) = (( - M) + ( 0. (K,( len M),( width M)))) by A1, A2, A3, MATRIX_3: 2;

        ( - M) is Matrix of ( len M), ( width M), K by A1, A2, A4, MATRIX_0: 20;

        hence thesis by A5, MATRIX_3: 4;

      end;

        suppose

         A6: ( len M) = 0 ;

        ( len (( 0. (K,( len M),( width M))) - M)) = ( len ( 0. (K,( len M),( width M)))) by MATRIX_3:def 3;

        hence thesis by A1, A3, A6, CARD_2: 64;

      end;

    end;

    theorem :: MATRIX_4:51

    for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds (M1 + M2) = (M1 - ( - M2)) by Th1;

    theorem :: MATRIX_4:52

    for K be Field, M1,M2 be Matrix of K st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds M1 = (M1 - (M2 + ( - M2)))

    proof

      let K be Field, M1,M2 be Matrix of K;

      assume ( len M1) = ( len M2) & ( width M1) = ( width M2);

      then M1 = (M1 - (M2 - M2)) by Th11;

      hence thesis;

    end;

    theorem :: MATRIX_4:53

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) & (M1 - M3) = (M2 + ( - M3)) holds M1 = M2

    proof

      let K be Field, M1,M2,M3 be Matrix of K;

      assume that

       A1: ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) and

       A2: (M1 - M3) = (M2 + ( - M3));

      (M1 - M3) = (M2 - M3) by A2;

      hence thesis by A1, Th14;

    end;

    theorem :: MATRIX_4:54

    for K be Field, M1,M2,M3 be Matrix of K st ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) & (M3 - M1) = (M3 + ( - M2)) holds M1 = M2

    proof

      let K be Field, M1,M2,M3 be Matrix of K such that

       A1: ( len M1) = ( len M2) & ( len M2) = ( len M3) & ( width M1) = ( width M2) & ( width M2) = ( width M3) and

       A2: (M3 - M1) = (M3 + ( - M2));

      (M3 - M1) = (M3 - M2) by A2;

      hence thesis by A1, Th15;

    end;

    theorem :: MATRIX_4:55



     Th55: for K be set, A,B be Matrix of K st ( len A) = ( len B) & ( width A) = ( width B) holds ( Indices A) = ( Indices B)

    proof

      let K be set, A,B be Matrix of K;



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

      assume ( len A) = ( len B) & ( width A) = ( width B);

      hence thesis by A1, FINSEQ_1:def 3;

    end;

    theorem :: MATRIX_4:56



     Th56: for K be Field, x,y,z be FinSequence of K st ( len x) = ( len y) & ( len y) = ( len z) holds ( mlt ((x + y),z)) = (( mlt (x,z)) + ( mlt (y,z)))

    proof

      let K be Field, x,y,z be FinSequence of K;

      assume that

       A1: ( len x) = ( len y) and

       A2: ( len y) = ( len z);



       A3: ( dom z) = ( Seg ( len x)) by A1, A2, FINSEQ_1:def 3;

      reconsider x2 = x, y2 = y, z2 = z as Element of (( len x) -tuples_on the carrier of K) by A1, A2, FINSEQ_2: 92;



       A4: ( dom (x + y)) = ( Seg ( len (x2 + y2))) by FINSEQ_1:def 3

      .= ( Seg ( len x)) by CARD_1:def 7

      .= ( dom z) by A1, A2, FINSEQ_1:def 3;



       A5: ( dom ( mlt (y,z))) = ( Seg ( len ( mlt (y2,z2)))) by FINSEQ_1:def 3

      .= ( Seg ( len x)) by CARD_1:def 7;



      then

       A6: ( dom ( mlt (y,z))) = ( Seg ( len (( mlt (x2,z2)) + ( mlt (y2,z2))))) by CARD_1:def 7

      .= ( dom (( mlt (x2,z2)) + ( mlt (y2,z2)))) by FINSEQ_1:def 3;



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



       A8: ( dom y) = ( Seg ( len x)) by A1, FINSEQ_1:def 3;



       A9: ( dom ( mlt (x,z))) = ( Seg ( len ( mlt (x2,z2)))) by FINSEQ_1:def 3

      .= ( Seg ( len x)) by CARD_1:def 7;



      then

       A10: ( dom ( mlt (x,z))) = ( Seg ( len (( mlt (x2,z2)) + ( mlt (y2,z2))))) by CARD_1:def 7

      .= ( dom (( mlt (x2,z2)) + ( mlt (y2,z2)))) by FINSEQ_1:def 3;



       A11: for i be Nat st i in ( dom ( mlt ((x + y),z))) holds (( mlt ((x + y),z)) . i) = ((( mlt (x,z)) + ( mlt (y,z))) . i)

      proof

        let i be Nat;



         A12: ( rng x) c= the carrier of K & ( rng y) c= the carrier of K by FINSEQ_1:def 4;



         A13: ( rng z) c= the carrier of K & ( rng (x + y)) c= the carrier of K by FINSEQ_1:def 4;

        ( dom the multF of K) = [:the carrier of K, the carrier of K:] by FUNCT_2:def 1;

        then ( mlt ((x + y),z)) = (the multF of K .: ((x + y),z)) & [:( rng (x + y)), ( rng z):] c= ( dom the multF of K) by A13, FVSUM_1:def 7, ZFMISC_1: 96;

        then

         A14: ( dom ( mlt ((x + y),z))) = (( dom (x + y)) /\ ( dom z)) by FUNCOP_1: 69;

        assume

         A15: i in ( dom ( mlt ((x + y),z)));

        then i in ( dom z) by A14, XBOOLE_0:def 4;

        then

         A16: (z . i) in ( rng z) by FUNCT_1:def 3;

        ( len (x2 + y2)) = ( len x) by CARD_1:def 7;

        then

         A17: ( dom (x2 + y2)) = ( Seg ( len x)) by FINSEQ_1:def 3;

        then

         A18: i in ( Seg ( len x)) by A15, A14, XBOOLE_0:def 4;

        then

         A19: ((x + y) . i) in ( rng (x + y)) by A17, FUNCT_1:def 3;

        i in ( dom y) by A1, A18, FINSEQ_1:def 3;

        then

         A20: (y . i) in ( rng y) by FUNCT_1:def 3;



         A21: i in ( dom x) by A18, FINSEQ_1:def 3;

        then (x . i) in ( rng x) by FUNCT_1:def 3;

        then

        reconsider a = (x . i), b = (y . i), d = ((x + y) . i), e = (z . i) as Element of K by A12, A13, A20, A16, A19;

        ( dom <:y, z:>) = (( dom x) /\ ( dom x)) by A8, A3, A7, FUNCT_3:def 7

        .= ( dom x);

        then

         A22: i in ( dom <:y, z:>) by A18, FINSEQ_1:def 3;

        ( dom [:y, z:]) = [:( dom y), ( dom z):] by FUNCT_3:def 8;

        then

         A23: [i, i] in ( dom [:y, z:]) by A8, A3, A15, A17, A14, ZFMISC_1: 87;

        ( dom [:y, z:]) = [:( dom y), ( dom z):] by FUNCT_3:def 8;

        then

         A24: [i, i] in ( dom [:y, z:]) by A8, A3, A15, A17, A14, ZFMISC_1: 87;

        ( dom the multF of K) = [:the carrier of K, the carrier of K:] by FUNCT_2:def 1;

        then [b, e] in ( dom the multF of K) by ZFMISC_1: 87;

        then ( dom (the multF of K * (y,z))) = ( dom (the multF of K * [:y, z:])) & ( [:y, z:] . (i,i)) in ( dom the multF of K) by A8, A3, A15, A17, A14, FINSEQOP:def 4, FUNCT_3:def 8;

        then [i, i] in ( dom (the multF of K * (y,z))) by A24, FUNCT_1: 11;



        then

         A25: (b * e) = ((the multF of K * (y,z)) . (i,i)) by FINSEQOP: 77

        .= ((the multF of K * [:y, z:]) . (i,i)) by FINSEQOP:def 4

        .= (the multF of K . ( [:y, z:] . (i,i))) by A23, FUNCT_1: 13

        .= (the multF of K . ((y . i),(z . i))) by A8, A3, A15, A17, A14, FUNCT_3:def 8

        .= (the multF of K . ( <:y, z:> . i)) by A8, A3, A15, A17, A14, FUNCT_3: 49

        .= ((the multF of K * <:y, z:>) . i) by A22, FUNCT_1: 13

        .= ((the multF of K .: (y,z)) . i) by FUNCOP_1:def 3

        .= (( mlt (y,z)) . i) by FVSUM_1:def 7;

        ( dom <:(x + y), z:>) = (( dom (x + y)) /\ ( dom z)) by FUNCT_3:def 7

        .= ( dom x) by A3, A4, FINSEQ_1:def 3;

        then

         A26: i in ( dom <:(x + y), z:>) by A18, FINSEQ_1:def 3;



         A27: (( mlt ((x + y),z)) . i) = ((the multF of K .: ((x + y),z)) . i) by FVSUM_1:def 7

        .= ((the multF of K * <:(x + y), z:>) . i) by FUNCOP_1:def 3

        .= (the multF of K . ( <:(x + y), z:> . i)) by A26, FUNCT_1: 13

        .= (d * e) by A4, A15, A14, FUNCT_3: 49;



         A28: ( dom <:( mlt (x,z)), ( mlt (y,z)):>) = (( dom ( mlt (x,z))) /\ ( dom ( mlt (y,z)))) by FUNCT_3:def 7

        .= ( dom x) by A9, A5, FINSEQ_1:def 3;



         A29: ( dom <:x, y:>) = (( dom x) /\ ( dom y)) by FUNCT_3:def 7

        .= ( dom x) by A8, A7;



         A30: (the addF of K .: (( mlt (x,z)),( mlt (y,z)))) = (( mlt (x,z)) + ( mlt (y,z))) by FVSUM_1:def 3;

        ( dom [:x, z:]) = [:( dom x), ( dom z):] by FUNCT_3:def 8;

        then

         A31: [i, i] in ( dom [:x, z:]) by A3, A7, A15, A17, A14, ZFMISC_1: 87;

        ( dom [:x, z:]) = [:( dom x), ( dom z):] by FUNCT_3:def 8;

        then

         A32: [i, i] in ( dom [:x, z:]) by A3, A7, A15, A17, A14, ZFMISC_1: 87;

        ( dom <:x, z:>) = (( dom x) /\ ( dom x)) by A3, A7, FUNCT_3:def 7

        .= ( dom x);

        then

         A33: i in ( dom <:x, z:>) by A18, FINSEQ_1:def 3;



         A34: ((x + y) . i) = ((the addF of K .: (x,y)) . i) by FVSUM_1:def 3

        .= ((the addF of K * <:x, y:>) . i) by FUNCOP_1:def 3

        .= (the addF of K . ( <:x, y:> . i)) by A21, A29, FUNCT_1: 13

        .= (a + b) by A8, A7, A18, FUNCT_3: 49;

        ( dom the multF of K) = [:the carrier of K, the carrier of K:] by FUNCT_2:def 1;

        then [a, e] in ( dom the multF of K) by ZFMISC_1: 87;

        then ( dom (the multF of K * (x,z))) = ( dom (the multF of K * [:x, z:])) & ( [:x, z:] . (i,i)) in ( dom the multF of K) by A3, A7, A15, A17, A14, FINSEQOP:def 4, FUNCT_3:def 8;

        then [i, i] in ( dom (the multF of K * (x,z))) by A32, FUNCT_1: 11;



        then (a * e) = ((the multF of K * (x,z)) . (i,i)) by FINSEQOP: 77

        .= ((the multF of K * [:x, z:]) . (i,i)) by FINSEQOP:def 4

        .= (the multF of K . ( [:x, z:] . (i,i))) by A31, FUNCT_1: 13

        .= (the multF of K . ((x . i),(z . i))) by A3, A7, A15, A17, A14, FUNCT_3:def 8

        .= (the multF of K . ( <:x, z:> . i)) by A3, A7, A15, A17, A14, FUNCT_3: 49

        .= ((the multF of K * <:x, z:>) . i) by A33, FUNCT_1: 13

        .= ((the multF of K .: (x,z)) . i) by FUNCOP_1:def 3

        .= (( mlt (x,z)) . i) by FVSUM_1:def 7;



        then ((a * e) + (b * e)) = (the addF of K . ( <:( mlt (x,z)), ( mlt (y,z)):> . i)) by A9, A10, A6, A18, A25, FUNCT_3: 49

        .= ((the addF of K * <:( mlt (x,z)), ( mlt (y,z)):>) . i) by A21, A28, FUNCT_1: 13

        .= ((( mlt (x,z)) + ( mlt (y,z))) . i) by A30, FUNCOP_1:def 3;

        hence thesis by A34, A27, VECTSP_1:def 7;

      end;

      ( dom ( mlt ((x + y),z))) = ( Seg ( len ( mlt ((x2 + y2),z2)))) by FINSEQ_1:def 3

      .= ( Seg ( len x)) by CARD_1:def 7

      .= ( Seg ( len (( mlt (x2,z2)) + ( mlt (y2,z2))))) by CARD_1:def 7

      .= ( dom (( mlt (x2,z2)) + ( mlt (y2,z2)))) by FINSEQ_1:def 3;

      hence thesis by A11, FINSEQ_1: 13;

    end;

    theorem :: MATRIX_4:57



     Th57: for K be Field, x,y,z be FinSequence of K st ( len x) = ( len y) & ( len y) = ( len z) holds ( mlt (z,(x + y))) = (( mlt (z,x)) + ( mlt (z,y)))

    proof

      let K be Field, x,y,z be FinSequence of K;

      assume

       A1: ( len x) = ( len y) & ( len y) = ( len z);

      then

      reconsider x2 = x, y2 = y, z2 = z as Element of (( len x) -tuples_on the carrier of K) by FINSEQ_2: 92;

      ( mlt (z,(x + y))) = ( mlt ((x2 + y2),z2)) by FVSUM_1: 63

      .= (( mlt (x2,z2)) + ( mlt (y,z))) by A1, Th56

      .= (( mlt (z,x)) + ( mlt (y2,z2))) by FVSUM_1: 63;

      hence thesis by FVSUM_1: 63;

    end;

    theorem :: MATRIX_4:58

    for D be non empty set, M be Matrix of D holds ( len M) > 0 implies for n be Nat holds M is Matrix of n, ( width M), D iff n = ( len M) by MATRIX_0: 20, MATRIX_0:def 2;

    theorem :: MATRIX_4:59



     Th59: for K be Field, j be Nat, A,B be Matrix of K st ( width A) = ( width B) & (ex j be Nat st [i, j] in ( Indices A)) holds ( Line ((A + B),i)) = (( Line (A,i)) + ( Line (B,i)))

    proof

      let K be Field, j be Nat, A,B be Matrix of K;

      assume that

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

       A2: ex j be Nat st [i, j] in ( Indices A);

      reconsider wA = ( width A) as Element of NAT by ORDINAL1:def 12;

      reconsider a = ( Line (A,i)), b = ( Line (B,i)) as Element of (wA -tuples_on the carrier of K) by A1;



       A3: ( width (A + B)) = ( width A) by MATRIX_3:def 3;

      i in ( dom A) by A2, ZFMISC_1: 87;

      then

       A4: i in ( Seg ( len A)) by FINSEQ_1:def 3;



       A5: ( len (A + B)) = ( len A) by MATRIX_3:def 3;

      then

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



       A7: for k be Nat st 1 <= k & k <= ( len ( Line ((A + B),i))) holds (( Line ((A + B),i)) . k) = ((( Line (A,i)) + ( Line (B,i))) . k)

      proof

        let k be Nat;

        assume

         A8: 1 <= k & k <= ( len ( Line ((A + B),i)));



         A9: ( len ( Line ((A + B),i))) = ( width A) by A3, MATRIX_0:def 7;

        then

         A10: k in ( Seg ( width (A + B))) by A3, A8, FINSEQ_1: 1;

        ( len ( Line (B,i))) = ( width B) by MATRIX_0:def 7;

        then k in ( Seg ( len ( Line (B,i)))) by A1, A8, A9, FINSEQ_1: 1;

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

        then

        reconsider e = (( Line (B,i)) . k) as Element of K by FINSEQ_2: 11;

        i in ( dom (A + B)) by A5, A4, FINSEQ_1:def 3;

        then

         A11: [i, k] in ( Indices (A + B)) by A10, ZFMISC_1: 87;



         A12: (( Line ((A + B),i)) . k) = ((A + B) * (i,k)) by A10, MATRIX_0:def 7

        .= ((A * (i,k)) + (B * (i,k))) by A6, A11, MATRIX_3:def 3;



         A13: ( len ( Line (A,i))) = ( width A) by MATRIX_0:def 7;

        then

         A14: k in ( Seg ( len ( Line (A,i)))) by A8, A9, FINSEQ_1: 1;

        then k in ( dom ( Line (A,i))) by FINSEQ_1:def 3;

        then

        reconsider d = (( Line (A,i)) . k) as Element of K by FINSEQ_2: 11;

        ( len (( Line (A,i)) + ( Line (B,i)))) = ( len (a + b))

        .= ( width A) by CARD_1:def 7

        .= ( len ( Line (A,i))) by CARD_1:def 7;

        then k in ( dom (( Line (A,i)) + ( Line (B,i)))) by A14, FINSEQ_1:def 3;

        then

         A15: ((( Line (A,i)) + ( Line (B,i))) . k) = (d + e) by FVSUM_1: 17;

        (( Line (A,i)) . k) = (A * (i,k)) by A13, A14, MATRIX_0:def 7;

        hence thesis by A1, A13, A12, A14, A15, MATRIX_0:def 7;

      end;



       A16: ( len (( Line (A,i)) + ( Line (B,i)))) = ( len (a + b))

      .= ( width A) by CARD_1:def 7;

      ( len ( Line ((A + B),i))) = ( width A) by A3, MATRIX_0:def 7;

      hence thesis by A16, A7, FINSEQ_1: 14;

    end;

    theorem :: MATRIX_4:60



     Th60: for K be Field, j be Nat, A,B be Matrix of K st ( len A) = ( len B) & (ex i st [i, j] in ( Indices A)) holds ( Col ((A + B),j)) = (( Col (A,j)) + ( Col (B,j)))

    proof

      let K be Field, j be Nat, A,B be Matrix of K;



       A1: ( len (A + B)) = ( len A) by MATRIX_3:def 3;

      assume

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

      then

      reconsider a = ( Col (A,j)), b = ( Col (B,j)) as Element of (( len A) -tuples_on the carrier of K);

      given i such that

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



       A4: ( width (A + B)) = ( width A) by MATRIX_3:def 3;

      then

       A5: ( Indices (A + B)) = ( Indices A) by A1, Th55;



       A6: for k be Nat st 1 <= k & k <= ( len ( Col ((A + B),j))) holds (( Col ((A + B),j)) . k) = ((( Col (A,j)) + ( Col (B,j))) . k)

      proof

        let k be Nat;

        assume

         A7: 1 <= k & k <= ( len ( Col ((A + B),j)));



         A8: ( len ( Col ((A + B),j))) = ( len A) by A1, MATRIX_0:def 8;

        then k in ( Seg ( len A)) by A7, FINSEQ_1: 1;

        then

         A9: k in ( dom (A + B)) by A1, FINSEQ_1:def 3;

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

        then k in ( Seg ( len ( Col (B,j)))) by A2, A7, A8, FINSEQ_1: 1;

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

        then

        reconsider e = (( Col (B,j)) . k) as Element of K by FINSEQ_2: 11;



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

        .= ( dom B) by A2, FINSEQ_1:def 3;



         A11: ( len ( Col (A,j))) = ( len A) by MATRIX_0:def 8;

        then

         A12: k in ( Seg ( len ( Col (A,j)))) by A7, A8, FINSEQ_1: 1;

        then k in ( dom ( Col (A,j))) by FINSEQ_1:def 3;

        then

        reconsider d = (( Col (A,j)) . k) as Element of K by FINSEQ_2: 11;

        ( len (( Col (A,j)) + ( Col (B,j)))) = ( len (a + b))

        .= ( len A) by CARD_1:def 7

        .= ( len ( Col (A,j))) by CARD_1:def 7;

        then k in ( dom (( Col (A,j)) + ( Col (B,j)))) by A12, FINSEQ_1:def 3;

        then

         A13: ((( Col (A,j)) + ( Col (B,j))) . k) = (d + e) by FVSUM_1: 17;

        j in ( Seg ( width (A + B))) by A3, A4, ZFMISC_1: 87;

        then

         A14: [k, j] in ( Indices (A + B)) by A9, ZFMISC_1: 87;



         A15: (( Col ((A + B),j)) . k) = ((A + B) * (k,j)) by A9, MATRIX_0:def 8

        .= ((A * (k,j)) + (B * (k,j))) by A5, A14, MATRIX_3:def 3;



         A16: k in ( dom A) by A11, A12, FINSEQ_1:def 3;

        then (( Col (A,j)) . k) = (A * (k,j)) by MATRIX_0:def 8;

        hence thesis by A15, A13, A10, A16, MATRIX_0:def 8;

      end;



       A17: ( len (( Col (A,j)) + ( Col (B,j)))) = ( len (a + b))

      .= ( len A) by CARD_1:def 7;

      ( len ( Col ((A + B),j))) = ( len A) by A1, MATRIX_0:def 8;

      hence thesis by A17, A6, FINSEQ_1: 14;

    end;

    theorem :: MATRIX_4:61



     Th61: for V1 be Field, P1,P2 be FinSequence of V1 st ( len P1) = ( len P2) holds ( Sum (P1 + P2)) = (( Sum P1) + ( Sum P2))

    proof

      let V1 be Field, P1,P2 be FinSequence of V1;

      assume ( len P1) = ( len P2);

      then

      reconsider R1 = P1, R2 = P2 as Element of (( len P1) -tuples_on the carrier of V1) by FINSEQ_2: 92;



      thus ( Sum (P1 + P2)) = ( Sum (R1 + R2))

      .= (( Sum P1) + ( Sum P2)) by FVSUM_1: 76;

    end;

    theorem :: MATRIX_4:62

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

    proof

      let K be Field, A,B,C be Matrix of K;

      assume that

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

       A2: ( width B) = ( width C) and

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

       A4: ( len A) > 0 and

       A5: ( len B) > 0 ;



       A6: ( len (B + C)) = ( len B) by MATRIX_3:def 3;

      then

       A7: ( len (A * (B + C))) = ( len A) by A3, MATRIX_3:def 4;



       A8: ( width (B + C)) = ( width B) & ( width (A * (B + C))) = ( width (B + C)) by A3, A6, MATRIX_3:def 3, MATRIX_3:def 4;

      then

      reconsider M1 = (A * (B + C)) as Matrix of ( len A), ( width B), K by A4, A7, MATRIX_0: 20;



       A9: ( len (A * B)) = ( len A) & ( width (A * B)) = ( width B) by A3, MATRIX_3:def 4;

      then

       A10: ( Indices M1) = ( Indices (A * B)) by A7, A8, Th55;



       A11: ( len ((A * B) + (A * C))) = ( len (A * B)) & ( width ((A * B) + (A * C))) = ( width (A * B)) by MATRIX_3:def 3;

      then

      reconsider M2 = ((A * B) + (A * C)) as Matrix of ( len A), ( width B), K by A4, A9, MATRIX_0: 20;

      ( len (A * C)) = ( len A) & ( width (A * C)) = ( width C) by A1, A3, MATRIX_3:def 4;

      then

       A12: ( Indices M1) = ( Indices (A * C)) by A2, A7, A8, Th55;

      for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (M2 * (i,j))

      proof

        let i, j;

        ( len ( Line (A,i))) = ( len B) by A3, MATRIX_0:def 7;

        then

         A13: ( len ( Line (A,i))) = ( len ( Col (B,j))) by MATRIX_0:def 8;

        reconsider q1 = ( Line (A,i)), q2 = ( Col (B,j)), q3 = ( Col (C,j)) as Element of (( len B) -tuples_on the carrier of K) by A1, A3;



         A14: ( len ( mlt (( Line (A,i)),( Col (B,j))))) = ( len ( mlt (q1,q2)))

        .= ( len B) by CARD_1:def 7

        .= ( len ( mlt (q1,q3))) by CARD_1:def 7

        .= ( len ( mlt (( Line (A,i)),( Col (C,j)))));

        ( dom B) = ( Seg ( len B)) & (1 + 0 ) <= ( len B) by A5, FINSEQ_1:def 3, NAT_1: 13;

        then

         A15: 1 in ( dom B) by FINSEQ_1: 1;

        ( len ( Line (A,i))) = ( len C) by A1, A3, MATRIX_0:def 7;

        then

         A16: ( len ( Line (A,i))) = ( len ( Col (C,j))) by MATRIX_0:def 8;

        assume

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



        then

         A18: (M2 * (i,j)) = (((A * B) * (i,j)) + ((A * C) * (i,j))) by A10, MATRIX_3:def 3

        .= ((( Line (A,i)) "*" ( Col (B,j))) + ((A * C) * (i,j))) by A3, A10, A17, MATRIX_3:def 4

        .= ((( Line (A,i)) "*" ( Col (B,j))) + (( Line (A,i)) "*" ( Col (C,j)))) by A1, A3, A12, A17, MATRIX_3:def 4

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

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

        j in ( Seg ( width B)) by A8, A17, ZFMISC_1: 87;

        then

         A19: [1, j] in ( Indices B) by A15, ZFMISC_1: 87;

        (M1 * (i,j)) = (( Line (A,i)) "*" ( Col ((B + C),j))) by A3, A6, A17, MATRIX_3:def 4

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

        .= ( Sum ( mlt (( Line (A,i)),(( Col (B,j)) + ( Col (C,j)))))) by A1, A19, Th60

        .= ( Sum (( mlt (( Line (A,i)),( Col (B,j)))) + ( mlt (( Line (A,i)),( Col (C,j)))))) by A13, A16, Th57

        .= (( Sum ( mlt (( Line (A,i)),( Col (B,j))))) + ( Sum ( mlt (( Line (A,i)),( Col (C,j)))))) by A14, Th61;

        hence thesis by A18;

      end;

      hence thesis by A7, A8, A9, A11, MATRIX_0: 21;

    end;

    theorem :: MATRIX_4:63

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

    proof

      let K be Field, A,B,C be Matrix of K;

      assume that

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

       A2: ( width B) = ( width C) and

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

       A4: ( len B) > 0 and

       A5: ( len A) > 0 ;



       A6: ( width (B + C)) = ( width B) by MATRIX_3:def 3;

      then

       A7: ( width ((B + C) * A)) = ( width A) by A3, MATRIX_3:def 4;

      ( len (B + C)) = ( len B) by MATRIX_3:def 3;

      then

       A8: ( len ((B + C) * A)) = ( len B) by A3, A6, MATRIX_3:def 4;

      then

      reconsider M1 = ((B + C) * A) as Matrix of ( len B), ( width A), K by A4, A7, MATRIX_0: 20;



       A9: ( len (B * A)) = ( len B) by A3, MATRIX_3:def 4;



       A10: ( width (B * A)) = ( width A) by A3, MATRIX_3:def 4;

      then

       A11: ( Indices M1) = ( Indices (B * A)) by A8, A7, A9, Th55;



       A12: ( len ((B * A) + (C * A))) = ( len (B * A)) & ( width ((B * A) + (C * A))) = ( width (B * A)) by MATRIX_3:def 3;

      then

      reconsider M2 = ((B * A) + (C * A)) as Matrix of ( len B), ( width A), K by A4, A9, A10, MATRIX_0: 20;

      ( len (C * A)) = ( len C) & ( width (C * A)) = ( width A) by A2, A3, MATRIX_3:def 4;

      then

       A13: ( Indices M1) = ( Indices (C * A)) by A1, A8, A7, Th55;

      for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (M2 * (i,j))

      proof

        let i, j;

        ( len ( Col (A,j))) = ( width B) by A3, MATRIX_0:def 8;

        then

         A14: ( len ( Col (A,j))) = ( len ( Line (B,i))) by MATRIX_0:def 7;

        reconsider q1 = ( Line (B,i)), q2 = ( Line (C,i)), q3 = ( Col (A,j)) as Element of (( len A) -tuples_on the carrier of K) by A2, A3;



         A15: ( len ( mlt (( Line (B,i)),( Col (A,j))))) = ( len ( mlt (q1,q3)))

        .= ( len A) by CARD_1:def 7

        .= ( len ( mlt (q2,q3))) by CARD_1:def 7

        .= ( len ( mlt (( Line (C,i)),( Col (A,j)))));

        (1 + 0 ) <= ( width B) by A3, A5, NAT_1: 13;

        then

         A16: 1 in ( Seg ( width B)) by FINSEQ_1: 1;

        ( len ( Col (A,j))) = ( width C) by A2, A3, MATRIX_0:def 8;

        then

         A17: ( len ( Col (A,j))) = ( len ( Line (C,i))) by MATRIX_0:def 7;

        assume

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



        then

         A19: (M2 * (i,j)) = (((B * A) * (i,j)) + ((C * A) * (i,j))) by A11, MATRIX_3:def 3

        .= ((( Line (B,i)) "*" ( Col (A,j))) + ((C * A) * (i,j))) by A3, A11, A18, MATRIX_3:def 4

        .= ((( Line (B,i)) "*" ( Col (A,j))) + (( Line (C,i)) "*" ( Col (A,j)))) by A2, A3, A13, A18, MATRIX_3:def 4

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

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

        i in ( dom (B * A)) by A11, A18, ZFMISC_1: 87;

        then i in ( Seg ( len B)) by A9, FINSEQ_1:def 3;

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

        then

         A20: [i, 1] in ( Indices B) by A16, ZFMISC_1: 87;

        (M1 * (i,j)) = (( Line ((B + C),i)) "*" ( Col (A,j))) by A3, A6, A18, MATRIX_3:def 4

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

        .= ( Sum ( mlt ((( Line (B,i)) + ( Line (C,i))),( Col (A,j))))) by A2, A20, Th59

        .= ( Sum (( mlt (( Line (B,i)),( Col (A,j)))) + ( mlt (( Line (C,i)),( Col (A,j)))))) by A14, A17, Th56

        .= (( Sum ( mlt (( Line (B,i)),( Col (A,j))))) + ( Sum ( mlt (( Line (C,i)),( Col (A,j)))))) by A15, Th61;

        hence thesis by A19;

      end;

      hence thesis by A8, A7, A9, A10, A12, MATRIX_0: 21;

    end;

    theorem :: MATRIX_4:64

    for K be Field, n,m,k be Nat, M1 be Matrix of n, m, K, M2 be Matrix of m, k, K st ( width M1) = ( len M2) & 0 < ( len M1) & 0 < ( len M2) holds (M1 * M2) is Matrix of n, k, K

    proof

      let K be Field, n,m,k be Nat, M1 be Matrix of n, m, K, M2 be Matrix of m, k, K;

      assume that

       A1: ( width M1) = ( len M2) and

       A2: 0 < ( len M1) and

       A3: 0 < ( len M2);

      ( width M1) = m by A1, MATRIX_0:def 2;

      then

       A4: ( len M1) = n & ( width M2) = k by A1, A3, MATRIX_0: 20, MATRIX_0:def 2;

      ( len (M1 * M2)) = ( len M1) & ( width (M1 * M2)) = ( width M2) by A1, MATRIX_3:def 4;

      hence thesis by A2, A4, MATRIX_0: 20;

    end;