matrixr1.miz



    begin

    reserve i,j for Nat;

    theorem :: MATRIXR1:1

    for r1,r2 be Real, fr1,fr2 be Element of F_Real st r1 = fr1 & r2 = fr2 holds (r1 + r2) = (fr1 + fr2);

    theorem :: MATRIXR1:2

    for r1,r2 be Real, fr1,fr2 be Element of F_Real st r1 = fr1 & r2 = fr2 holds (r1 * r2) = (fr1 * fr2);

    theorem :: MATRIXR1:3

    

     Th3: for F be FinSequence of REAL holds (F + ( - F)) = ( 0* ( len F)) & (F - F) = ( 0* ( len F))

    proof

      let F be FinSequence of REAL ;

      set n = ( len F);

      reconsider R = F as Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

      

       A1: (R + ( - R)) = (n |-> 0 qua Real) by RVSUM_1: 22;

      hence (F + ( - F)) = ( 0* ( len F)) by EUCLID:def 4;

      thus thesis by A1, EUCLID:def 4;

    end;

    theorem :: MATRIXR1:4

    for F1,F2 be FinSequence of REAL st ( len F1) = ( len F2) holds (F1 - F2) = (F1 + ( - F2));

    theorem :: MATRIXR1:5

    for F be FinSequence of REAL holds (F - ( 0* ( len F))) = F

    proof

      let F be FinSequence of REAL ;

      set n = ( len F);

      reconsider R = F as Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

      (R - (n |-> 0 qua Real)) = R by RVSUM_1: 32;

      hence thesis by EUCLID:def 4;

    end;

    theorem :: MATRIXR1:6

    for F be FinSequence of REAL holds (( 0* ( len F)) - F) = ( - F)

    proof

      let F be FinSequence of REAL ;

      set n = ( len F);

      reconsider R = F as Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

      ((n |-> 0 qua Real) - R) = ( - R) by RVSUM_1: 33;

      hence thesis by EUCLID:def 4;

    end;

    theorem :: MATRIXR1:7

    for F1,F2 be FinSequence of REAL st ( len F1) = ( len F2) holds (F1 - ( - F2)) = (F1 + F2);

    theorem :: MATRIXR1:8

    for F1,F2 be FinSequence of REAL st ( len F1) = ( len F2) holds ( - (F1 - F2)) = (F2 - F1) by RVSUM_1: 35;

    theorem :: MATRIXR1:9

    for F1,F2 be FinSequence of REAL st ( len F1) = ( len F2) holds ( - (F1 - F2)) = (( - F1) + F2) by RVSUM_1: 36;

    theorem :: MATRIXR1:10

    for F1,F2 be FinSequence of REAL st ( len F1) = ( len F2) & (F1 - F2) = ( 0* ( len F1)) holds F1 = F2

    proof

      let F1,F2 be FinSequence of REAL ;

      set n = ( len F1);

      assume ( len F1) = ( len F2);

      then

      reconsider R1 = F1, R2 = F2 as Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

      (R1 - R2) = (n |-> 0 ) implies R1 = R2 by RVSUM_1: 38;

      hence thesis by EUCLID:def 4;

    end;

    theorem :: MATRIXR1:11

    for F1,F2,F3 be FinSequence of REAL st ( len F1) = ( len F2) & ( len F2) = ( len F3) holds ((F1 - F2) - F3) = (F1 - (F2 + F3)) by RVSUM_1: 39;

    theorem :: MATRIXR1:12

    for F1,F2,F3 be FinSequence of REAL st ( len F1) = ( len F2) & ( len F2) = ( len F3) holds (F1 + (F2 - F3)) = ((F1 + F2) - F3) by RVSUM_1: 40;

    theorem :: MATRIXR1:13

    for F1,F2,F3 be FinSequence of REAL st ( len F1) = ( len F2) & ( len F2) = ( len F3) holds (F1 - (F2 - F3)) = ((F1 - F2) + F3) by RVSUM_1: 41;

    theorem :: MATRIXR1:14

    

     Th14: for F1,F2 be FinSequence of REAL st ( len F1) = ( len F2) holds F1 = ((F1 + F2) - F2)

    proof

      let F1,F2 be FinSequence of REAL ;

      set n = ( len F1);

      assume ( len F1) = ( len F2);

      then

      reconsider R1 = F1, R2 = F2 as Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

      R1 = ((R1 + R2) - R2) by RVSUM_1: 42;

      hence thesis;

    end;

    theorem :: MATRIXR1:15

    for F1,F2 be FinSequence of REAL st ( len F1) = ( len F2) holds F1 = ((F1 - F2) + F2)

    proof

      let F1,F2 be FinSequence of REAL ;

      set n = ( len F1);

      assume ( len F1) = ( len F2);

      then

      reconsider R1 = F1, R2 = F2 as Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

      R1 = ((R1 - R2) + R2) by RVSUM_1: 43;

      hence thesis;

    end;

    begin

    theorem :: MATRIXR1:16

    

     Th16: for K be non empty multMagma, p be FinSequence of K, a be Element of K holds ( len (a * p)) = ( len p)

    proof

      let K be non empty multMagma, p be FinSequence of K, a be Element of K;

      reconsider q = p as Element of (( len p) -tuples_on the carrier of K) by FINSEQ_2: 92;

      (a * q) in (( len p) -tuples_on the carrier of K);

      then (a * q) in { s where s be Element of (the carrier of K * ) : ( len s) = ( len p) } by FINSEQ_2:def 4;

      then ex s be Element of (the carrier of K * ) st (a * q) = s & ( len s) = ( len p);

      hence thesis;

    end;

    theorem :: MATRIXR1:17

    

     Th17: for r be Real, fr be Element of F_Real , p be FinSequence of REAL , fp be FinSequence of F_Real st r = fr & p = fp holds (r * p) = (fr * fp)

    proof

      let r be Real, fr be Element of F_Real , p be FinSequence of REAL , fp be FinSequence of F_Real ;

      assume that

       A1: r = fr and

       A2: p = fp;

      

       A3: ( len (r * p)) = ( len fp) by A2, RVSUM_1: 117;

      then

       A4: ( len (r * p)) = ( len (fr * fp)) by Th16;

      for i be Nat st 1 <= i & i <= ( len (r * p)) holds ((r * p) . i) = ((fr * fp) . i)

      proof

        let i be Nat;

        assume 1 <= i & i <= ( len (r * p));

        then i in ( Seg ( len fp)) by A3, FINSEQ_1: 1;

        then

         A5: i in ( dom (fr * fp)) by A3, A4, FINSEQ_1:def 3;

        reconsider s = (fp . i) as Element of F_Real by XREAL_0:def 1;

        

        thus ((r * p) . i) = (fr * s) by A1, A2, RVSUM_1: 44

        .= ((fr * fp) . i) by A5, FVSUM_1: 50;

      end;

      hence thesis by A4, FINSEQ_1: 14;

    end;

    theorem :: MATRIXR1:18

    for K be Field, a be Element of K, A be Matrix of K holds ( Indices (a * A)) = ( Indices A)

    proof

      let K be Field, a be Element of K, A be Matrix of K;

      ( len (a * A)) = ( len A) & ( width (a * A)) = ( width A) by MATRIX_3:def 5;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: MATRIXR1:19

    

     Th19: for K be Field, a be Element of K, M be Matrix of K st 1 <= i & i <= ( width M) holds ( Col ((a * M),i)) = (a * ( Col (M,i)))

    proof

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

      assume

       A1: 1 <= i & i <= ( width M);

      

       A2: ( Seg ( len (a * M))) = ( dom (a * M)) by FINSEQ_1:def 3;

      

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

      then

       A4: ( dom M) = ( dom (a * M)) by FINSEQ_3: 29;

      

       A5: ( len (a * ( Col (M,i)))) = ( len ( Col (M,i))) & ( len ( Col (M,i))) = ( len M) by Th16, MATRIX_0:def 8;

      then

       A6: ( dom (a * ( Col (M,i)))) = ( Seg ( len (a * M))) by A3, FINSEQ_1:def 3;

      for j st j in ( dom (a * M)) holds ((a * ( Col (M,i))) . j) = ((a * M) * (j,i))

      proof

        let j;

        assume

         A7: j in ( dom (a * M));

        i in ( Seg ( width M)) by A1, FINSEQ_1: 1;

        then [j, i] in ( Indices M) by A4, A7, ZFMISC_1: 87;

        then

         A8: ((a * M) * (j,i)) = (a * (M * (j,i))) by MATRIX_3:def 5;

        (( Col (M,i)) . j) = (M * (j,i)) by A4, A7, MATRIX_0:def 8;

        hence thesis by A6, A2, A7, A8, FVSUM_1: 50;

      end;

      hence thesis by A5, A3, MATRIX_0:def 8;

    end;

    theorem :: MATRIXR1:20

    for K be Field, a be Element of K, M be Matrix of K, i be Nat st 1 <= i & i <= ( len M) holds ( Line ((a * M),i)) = (a * ( Line (M,i)))

    proof

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

      let i be Nat;

      assume

       A1: 1 <= i & i <= ( len M);

      

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

      

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

      

       A4: ( len (a * ( Line (M,i)))) = ( len ( Line (M,i))) & ( len ( Line (M,i))) = ( width M) by Th16, MATRIX_0:def 7;

      then

       A5: ( dom (a * ( Line (M,i)))) = ( Seg ( width (a * M))) by A2, FINSEQ_1:def 3;

      for j st j in ( Seg ( width (a * M))) holds ((a * ( Line (M,i))) . j) = ((a * M) * (i,j))

      proof

        let j;

        assume

         A6: j in ( Seg ( width (a * M)));

        i in ( dom M) by A1, FINSEQ_3: 25;

        then [i, j] in ( Indices M) by A3, A6, ZFMISC_1: 87;

        then

         A7: ((a * M) * (i,j)) = (a * (M * (i,j))) by MATRIX_3:def 5;

        (( Line (M,i)) . j) = (M * (i,j)) by A3, A6, MATRIX_0:def 7;

        hence thesis by A5, A6, A7, FVSUM_1: 50;

      end;

      hence thesis by A4, A2, MATRIX_0:def 7;

    end;

    theorem :: MATRIXR1:21

    for K be Field, A,B be Matrix of K st ( width A) = ( len B) holds ex C be Matrix of K st ( len C) = ( len A) & ( width C) = ( width B) & for i, j st [i, j] in ( Indices C) holds (C * (i,j)) = (( Line (A,i)) "*" ( Col (B,j)))

    proof

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

      assume

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

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

      consider M be Matrix of ( len A), ( width B), the carrier of 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;

      per cases ;

        suppose ( len A) > 0 ;

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

        hence thesis by A2;

      end;

        suppose

         A3: ( len A) = 0 ;

        then

         A4: ( len M) = 0 by MATRIX_0: 25;

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

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

        then ( width M) = ( width B) by A4, MATRIX_0:def 3;

        hence thesis by A2, A3, A4;

      end;

    end;

    theorem :: MATRIXR1:22

    

     Th22: for K be Field, a be Element of K, A,B be Matrix of K st ( width A) = ( len B) holds (A * (a * B)) = (a * (A * B))

    proof

      let K be Field, a be Element of K, A,B be Matrix of K;

      set C = (a * B);

      set D = (a * (A * B));

      

       A1: ( len D) = ( len (A * B)) by MATRIX_3:def 5;

      assume

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

      then ( width (A * B)) = ( width B) by MATRIX_3:def 4;

      

      then

       A3: ( width D) = ( width B) by MATRIX_3:def 5

      .= ( width C) by MATRIX_3:def 5;

      

       A4: ( width B) = ( width (a * B)) by MATRIX_3:def 5;

      

       A5: for i, j st [i, j] in ( Indices D) holds (D * (i,j)) = (( Line (A,i)) "*" ( Col (C,j)))

      proof

        let i, j;

        reconsider xo = ( Col (B,j)) as Element of (( width A) -tuples_on the carrier of K) by A2;

        assume

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

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

        then

         A7: 1 <= j & j <= ( width B) by FINSEQ_1: 1;

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

        then

         A8: [i, j] in ( Indices (A * B)) by A6, MATRIX_3:def 5;

        then ((a * (A * B)) * (i,j)) = (a * ((A * B) * (i,j))) by MATRIX_3:def 5;

        

        then ((a * (A * B)) * (i,j)) = (a * (( Line (A,i)) "*" ( Col (B,j)))) by A2, A8, MATRIX_3:def 4

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

        .= ( Sum (a * ( mlt (( Line (A,i)),( Col (B,j)))))) by FVSUM_1: 73

        .= ( Sum ( mlt (( Line (A,i)),(a * xo)))) by FVSUM_1: 69

        .= ( Sum ( mlt (( Line (A,i)),( Col ((a * B),j))))) by A7, Th19;

        hence thesis by FVSUM_1:def 9;

      end;

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

      hence thesis by A2, A1, A3, A5, MATRIX_3:def 4;

    end;

    definition

      let A be Matrix of REAL ;

      :: MATRIXR1:def1

      func MXR2MXF A -> Matrix of F_Real equals A;

      coherence ;

    end

    definition

      let A be Matrix of F_Real ;

      :: MATRIXR1:def2

      func MXF2MXR A -> Matrix of REAL equals A;

      coherence ;

    end

    theorem :: MATRIXR1:23

    for D1,D2 be set, A be Matrix of D1, B be Matrix of D2 st A = B holds for i, j st [i, j] in ( Indices A) holds (A * (i,j)) = (B * (i,j))

    proof

      let D1,D2 be set, A be Matrix of D1, B be Matrix of D2;

      assume

       A1: A = B;

      let i, j;

      assume

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

      then

       A3: ex p be FinSequence of D1 st p = (A . i) & (A * (i,j)) = (p . j) by MATRIX_0:def 5;

      ex q be FinSequence of D2 st q = (B . i) & (B * (i,j)) = (q . j) by A1, A2, MATRIX_0:def 5;

      hence thesis by A1, A3;

    end;

    theorem :: MATRIXR1:24

    for K be Field, A,B be Matrix of K holds ( Indices (A + B)) = ( Indices A)

    proof

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

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

      hence thesis by MATRIX_4: 55;

    end;

    definition

      let A,B be Matrix of REAL ;

      :: MATRIXR1:def3

      func A + B -> Matrix of REAL equals ( MXF2MXR (( MXR2MXF A) + ( MXR2MXF B)));

      coherence ;

    end

    theorem :: MATRIXR1:25

    

     Th25: for A,B be Matrix of REAL holds ( len (A + B)) = ( len A) & ( width (A + B)) = ( width A) & for i, j holds [i, j] in ( Indices A) implies ((A + B) * (i,j)) = ((A * (i,j)) + (B * (i,j)))

    proof

      let A,B be Matrix of REAL ;

      thus ( len (A + B)) = ( len A) & ( width (A + B)) = ( width A) by MATRIX_3:def 3;

      let i, j;

      assume [i, j] in ( Indices A);

      then ((A + B) * (i,j)) = ((( MXR2MXF A) * (i,j)) + (( MXR2MXF B) * (i,j))) by MATRIX_3:def 3;

      hence thesis;

    end;

    theorem :: MATRIXR1:26

    

     Th26: for A,B,C be Matrix of REAL st ( len C) = ( len A) & ( width C) = ( width A) & for i, j st [i, j] in ( Indices A) holds (C * (i,j)) = ((A * (i,j)) + (B * (i,j))) holds C = (A + B)

    proof

      let A,B,C be Matrix of REAL ;

      assume that

       A1: ( len C) = ( len A) & ( width C) = ( width A) and

       A2: for i, j holds [i, j] in ( Indices A) implies (C * (i,j)) = ((A * (i,j)) + (B * (i,j)));

      set B2 = ( MXR2MXF B);

      set A2 = ( MXR2MXF A);

      set D = ( MXR2MXF C);

      for i, j st [i, j] in ( Indices A2) holds (D * (i,j)) = ((A2 * (i,j)) + (B2 * (i,j))) by A2;

      hence thesis by A1, MATRIX_3:def 3;

    end;

    definition

      let A be Matrix of REAL ;

      :: MATRIXR1:def4

      func - A -> Matrix of REAL equals ( MXF2MXR ( - ( MXR2MXF A)));

      coherence ;

    end

    definition

      let A,B be Matrix of REAL ;

      :: MATRIXR1:def5

      func A - B -> Matrix of REAL equals ( MXF2MXR (( MXR2MXF A) - ( MXR2MXF B)));

      coherence ;

      :: MATRIXR1:def6

      func A * B -> Matrix of REAL equals ( MXF2MXR (( MXR2MXF A) * ( MXR2MXF B)));

      coherence ;

    end

    definition

      let a be Real, A be Matrix of REAL ;

      :: MATRIXR1:def7

      func a * A -> Matrix of REAL means

      : Def7: for ea be Element of F_Real st ea = a holds it = ( MXF2MXR (ea * ( MXR2MXF A)));

      existence

      proof

        reconsider aa = a as Element of F_Real by XREAL_0:def 1;

        set C = ( MXF2MXR (aa * ( MXR2MXF A)));

        for ea be Element of F_Real st ea = a holds C = ( MXF2MXR (ea * ( MXR2MXF A)));

        hence thesis;

      end;

      uniqueness

      proof

        reconsider aa = a as Element of F_Real by XREAL_0:def 1;

        let C1,C2 be Matrix of REAL ;

        assume that

         A1: for ea be Element of F_Real st ea = a holds C1 = ( MXF2MXR (ea * ( MXR2MXF A))) and

         A2: for ea be Element of F_Real st ea = a holds C2 = ( MXF2MXR (ea * ( MXR2MXF A)));

        C2 = ( MXF2MXR (aa * ( MXR2MXF A))) by A2;

        hence thesis by A1;

      end;

    end

    theorem :: MATRIXR1:27

    

     Th27: for a be Real, A be Matrix of REAL holds ( len (a * A)) = ( len A) & ( width (a * A)) = ( width A)

    proof

      let a be Real, A be Matrix of REAL ;

      reconsider ea = a as Element of F_Real by XREAL_0:def 1;

      

      thus ( len (a * A)) = ( len ( MXF2MXR (ea * ( MXR2MXF A)))) by Def7

      .= ( len A) by MATRIX_3:def 5;

      

      thus ( width (a * A)) = ( width ( MXF2MXR (ea * ( MXR2MXF A)))) by Def7

      .= ( width A) by MATRIX_3:def 5;

    end;

    theorem :: MATRIXR1:28

    

     Th28: for a be Real, A be Matrix of REAL holds ( Indices (a * A)) = ( Indices A)

    proof

      let a be Real, A be Matrix of REAL ;

      ( len A) = ( len (a * A)) & ( width (a * A)) = ( width A) by Th27;

      hence thesis by MATRIX_4: 55;

    end;

    theorem :: MATRIXR1:29

    

     Th29: for a be Real, A be Matrix of REAL , i2,j2 be Nat st [i2, j2] in ( Indices A) holds ((a * A) * (i2,j2)) = (a * (A * (i2,j2)))

    proof

      let a be Real, A be Matrix of REAL ;

      let i2,j2 be Nat;

      reconsider ea = a as Element of F_Real by XREAL_0:def 1;

      assume [i2, j2] in ( Indices A);

      

      then (( MXF2MXR (ea * ( MXR2MXF A))) * (i2,j2)) = (ea * (( MXR2MXF A) * (i2,j2))) by MATRIX_3:def 5

      .= (a * (A * (i2,j2)));

      hence thesis by Def7;

    end;

    theorem :: MATRIXR1:30

    

     Th30: for a be Real, A be Matrix of REAL st ( width A) > 0 holds ((a * A) @ ) = (a * (A @ ))

    proof

      let a be Real, A be Matrix of REAL ;

      assume ( width A) > 0 ;

      then

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

      

       A2: for i, j holds [i, j] in ( Indices (a * (A @ ))) iff [j, i] in ( Indices (a * A))

      proof

        let i, j;

        ( Indices (a * (A @ ))) = ( Indices (A @ )) & ( Indices (a * A)) = ( Indices A) by Th28;

        hence thesis by MATRIX_0:def 6;

      end;

      

       A3: for i, j st [j, i] in ( Indices (a * A)) holds ((a * (A @ )) * (i,j)) = ((a * A) * (j,i))

      proof

        let i, j;

        assume [j, i] in ( Indices (a * A));

        then

         A4: [j, i] in ( Indices A) by Th28;

        then [i, j] in ( Indices (A @ )) by MATRIX_0:def 6;

        then ((a * (A @ )) * (i,j)) = (a * ((A @ ) * (i,j))) by Th29;

        

        then ((a * (A @ )) * (i,j)) = (a * (A * (j,i))) by A4, MATRIX_0:def 6

        .= ((a * A) * (j,i)) by A4, Th29;

        hence thesis;

      end;

      ( len (a * (A @ ))) = ( len (A @ )) & ( width A) = ( width (a * A)) by Th27;

      hence thesis by A1, A2, A3, MATRIX_0:def 6;

    end;

    theorem :: MATRIXR1:31

    for a be Real, i be Nat, A be Matrix of REAL st ( len A) > 0 & i in ( dom A) holds (ex p be FinSequence of REAL st p = (A . i)) & for q be FinSequence of REAL st q = (A . i) holds ((a * A) . i) = (a * q)

    proof

      let a be Real, i be Nat, A be Matrix of REAL ;

      assume that

       A1: ( len A) > 0 and

       A2: i in ( dom A);

      consider n3 be Nat such that

       A3: for x be object st x in ( rng A) holds ex s2 be FinSequence st s2 = x & ( len s2) = n3 by MATRIX_0:def 1;

      (A . i) in ( rng A) by A2, FUNCT_1:def 3;

      then

       A4: ex qq0 be FinSequence st qq0 = (A . i) & ( len qq0) = n3 by A3;

      ( len (a * A)) = ( len A) by Th27;

      then

      consider s be FinSequence such that

       A5: s in ( rng (a * A)) and

       A6: ( len s) = ( width (a * A)) by A1, MATRIX_0:def 3;

      

       A7: ( width (a * A)) = ( width A) by Th27;

      consider s3 be FinSequence such that

       A8: s3 in ( rng A) and

       A9: ( len s3) = ( width A) by A1, MATRIX_0:def 3;

      consider n2 be Nat such that

       A10: for x be object st x in ( rng (a * A)) holds ex s2 be FinSequence st s2 = x & ( len s2) = n2 by MATRIX_0:def 1;

      ( len (a * A)) = ( len A) by Th27;

      then

       A11: ( dom (a * A)) = ( dom A) by FINSEQ_3: 29;

      then ((a * A) . i) in ( rng (a * A)) by A2, FUNCT_1:def 3;

      then

      consider qq be FinSequence such that

       A12: qq = ((a * A) . i) and

       A13: ( len qq) = n2 by A10;

      consider n be Nat such that

       A14: for x be object st x in ( rng A) holds ex p be FinSequence of REAL st x = p & ( len p) = n by MATRIX_0: 9;

      (A . i) in ( rng A) by A2, FUNCT_1:def 3;

      then ex p2 be FinSequence of REAL st (A . i) = p2 & ( len p2) = n by A14;

      hence ex p be FinSequence of REAL st p = (A . i);

      let q be FinSequence of REAL ;

      assume

       A15: q = (A . i);

      

       A16: ex s4 be FinSequence st s4 = s3 & ( len s4) = n3 by A8, A3;

      then

       A17: ( len (a * q)) = ( width A) by A15, A9, A4, RVSUM_1: 117;

      

       A18: for j be Nat st 1 <= j & j <= ( len (a * q)) holds (qq . j) = ((a * q) . j)

      proof

        let j be Nat;

        assume 1 <= j & j <= ( len (a * q));

        then

         A19: j in ( Seg ( width A)) by A17, FINSEQ_1: 1;

        then

         A20: [i, j] in ( Indices A) by A2, ZFMISC_1: 87;

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

         [i, j] in ( Indices (a * A)) by A2, A7, A11, A19, ZFMISC_1: 87;

        then

         A21: ex p be FinSequence of REAL st p = ((a * A) . i) & ((a * A) * (i,j)) = (p . j) by MATRIX_0:def 5;

        ex p2 be FinSequence of REAL st p2 = (A . i) & (A * (i,j)) = (p2 . j) by A20, MATRIX_0:def 5;

        then (qq . j) = (a * (q . j)) by A15, A12, A20, A21, Th29;

        hence thesis by RVSUM_1: 44;

      end;

      ex s2 be FinSequence st s2 = s & ( len s2) = n2 by A5, A10;

      then ( width A) = ( len qq) by A6, A13, Th27;

      hence thesis by A15, A9, A16, A12, A4, A18, FINSEQ_1: 14, RVSUM_1: 117;

    end;

    theorem :: MATRIXR1:32

    for A be Matrix of REAL holds (1 * A) = A

    proof

      let A be Matrix of REAL ;

      (1 * A) = ( MXF2MXR (( 1_ F_Real ) * ( MXR2MXF A))) by Def7;

      hence thesis by MATRIX_5: 9;

    end;

    theorem :: MATRIXR1:33

    for A be Matrix of REAL holds (A + A) = (2 * A)

    proof

      set e2 = (( 1_ F_Real ) + ( 1_ F_Real ));

      let A be Matrix of REAL ;

      

       A1: (( 1_ F_Real ) * ( MXR2MXF A)) = ( MXR2MXF A) by MATRIX_5: 9;

      (2 * A) = ( MXF2MXR (e2 * ( MXR2MXF A))) by Def7

      .= ( MXF2MXR (( MXR2MXF A) + ( MXR2MXF A))) by A1, MATRIX_5: 12;

      hence thesis;

    end;

    theorem :: MATRIXR1:34

    for A be Matrix of REAL holds ((A + A) + A) = (3 * A)

    proof

      reconsider e3 = ((( 1_ F_Real ) + ( 1_ F_Real )) + ( 1_ F_Real )) as Element of F_Real ;

      let A be Matrix of REAL ;

      

       A1: ( len A) = ( len ( MXR2MXF A)) & ( width A) = ( width ( MXR2MXF A));

      (3 * A) = ( MXF2MXR (e3 * ( MXR2MXF A))) by Def7

      .= ( MXF2MXR ((( 1_ F_Real ) * ( MXR2MXF A)) + ((( 1_ F_Real ) + ( 1_ F_Real )) * ( MXR2MXF A)))) by MATRIX_5: 12

      .= ( MXF2MXR (( MXR2MXF A) + ((( 1_ F_Real ) + ( 1_ F_Real )) * ( MXR2MXF A)))) by MATRIX_5: 9

      .= ( MXF2MXR (( MXR2MXF A) + ((( 1_ F_Real ) * ( MXR2MXF A)) + (( 1_ F_Real ) * ( MXR2MXF A))))) by MATRIX_5: 12

      .= ( MXF2MXR (( MXR2MXF A) + (( MXR2MXF A) + (( 1_ F_Real ) * ( MXR2MXF A))))) by MATRIX_5: 9

      .= ( MXF2MXR (( MXR2MXF A) + (( MXR2MXF A) + ( MXR2MXF A)))) by MATRIX_5: 9

      .= ( MXF2MXR ((( MXR2MXF A) + ( MXR2MXF A)) + ( MXR2MXF A))) by A1, MATRIX_3: 3;

      hence thesis;

    end;

    definition

      let n,m be Nat;

      :: MATRIXR1:def8

      func 0_Rmatrix (n,m) -> Matrix of REAL equals ( MXF2MXR ( 0. ( F_Real ,n,m)));

      coherence ;

    end

    theorem :: MATRIXR1:35

    for A,B be Matrix of REAL holds (A - ( - B)) = (A + B)

    proof

      let A,B be Matrix of REAL ;

      (A + B) = ( MXF2MXR (( MXR2MXF A) + ( MXR2MXF ( - ( - B))))) by MATRIX_4: 1;

      hence thesis by MATRIX_4:def 1;

    end;

    theorem :: MATRIXR1:36

    

     Th36: for n,m be Nat, A be Matrix of REAL st ( len A) = n & ( width A) = m & n > 0 holds (A + ( 0_Rmatrix (n,m))) = A & (( 0_Rmatrix (n,m)) + A) = A

    proof

      let n,m be Nat, A be Matrix of REAL ;

      assume that

       A1: ( len A) = n & ( width A) = m and

       A2: n > 0 ;

      reconsider D = ( MXR2MXF A) as Matrix of n, m, F_Real by A1, A2, MATRIX_0: 20;

      ( len ( 0. ( F_Real ,n,m))) = n & ( width ( 0. ( F_Real ,n,m))) = m by A2, MATRIX_0: 23;

      

      then

       A3: (( 0_Rmatrix (n,m)) + A) = ( MXF2MXR (D + ( 0. ( F_Real ,n,m)))) by A1, MATRIX_3: 2

      .= A by MATRIX_3: 4;

      ( MXR2MXF A) is Matrix of n, m, F_Real by A1, A2, MATRIX_0: 20;

      hence thesis by A3, MATRIX_3: 4;

    end;

    theorem :: MATRIXR1:37

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

    proof

      let A,B be Matrix of REAL ;

      assume that

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

       A2: A = (A + B);

      ( 0_Rmatrix (( len A),( width A))) = ((A + B) + ( - A)) by A2, MATRIX_4: 2

      .= ( MXF2MXR ((( MXR2MXF B) + ( MXR2MXF A)) + ( - ( MXR2MXF A)))) by A1, MATRIX_3: 2

      .= ( MXF2MXR ((( MXR2MXF B) + ( MXR2MXF A)) - ( MXR2MXF A))) by MATRIX_4:def 1

      .= B by A1, MATRIX_4: 21;

      hence thesis;

    end;

    theorem :: MATRIXR1:38

    for A,B be Matrix of REAL st ( len A) = ( len B) & ( width A) = ( width B) & (A + B) = ( 0_Rmatrix (( len A),( width A))) holds B = ( - A)

    proof

      let A,B be Matrix of REAL ;

      assume that

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

       A2: (A + B) = ( 0_Rmatrix (( len A),( width A)));

      

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

      ( MXR2MXF ( 0_Rmatrix (( len A),( width A)))) = (( MXR2MXF A) + ( - ( - ( MXR2MXF B)))) by A2, MATRIX_4: 1

      .= (( MXR2MXF A) - ( - ( MXR2MXF B))) by MATRIX_4:def 1;

      then ( MXR2MXF A) = ( - ( MXR2MXF B)) by A1, A3, MATRIX_4: 7;

      hence thesis by MATRIX_4: 1;

    end;

    theorem :: MATRIXR1:39

    for A,B be Matrix of REAL st ( len A) = ( len B) & ( width A) = ( width B) & (B - A) = B holds A = ( 0_Rmatrix (( len A),( width A)))

    proof

      let A,B be Matrix of REAL ;

      assume that

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

       A2: (B - A) = B;

      (( MXR2MXF B) + ( MXR2MXF A)) = ( MXR2MXF B) by A1, A2, MATRIX_4: 22;

      hence thesis by A1, MATRIX_4: 6;

    end;

    theorem :: MATRIXR1:40

    

     Th40: for a be Real, A,B be Matrix of REAL st ( width A) = ( len B) holds (A * (a * B)) = (a * (A * B))

    proof

      let a be Real, A,B be Matrix of REAL ;

      assume

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

      reconsider ea = a as Element of F_Real by XREAL_0:def 1;

      

      thus (A * (a * B)) = ( MXF2MXR (( MXR2MXF A) * ( MXR2MXF ( MXF2MXR (ea * ( MXR2MXF B)))))) by Def7

      .= ( MXF2MXR (ea * ( MXR2MXF ( MXF2MXR (( MXR2MXF A) * ( MXR2MXF B)))))) by A1, Th22

      .= (a * (A * B)) by Def7;

    end;

    theorem :: MATRIXR1:41

    for a be Real, A,B be Matrix of REAL st ( width A) = ( len B) & ( len A) > 0 & ( len B) > 0 & ( width B) > 0 holds ((a * A) * B) = (a * (A * B))

    proof

      let a be Real, A,B be Matrix of REAL ;

      assume that

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

       A2: ( len A) > 0 and

       A3: ( len B) > 0 and

       A4: ( width B) > 0 ;

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

      then ((B @ ) * (a * (A @ ))) = (a * ((B @ ) * (A @ ))) by A1, Th40;

      then

       A5: ((B @ ) * (a * (A @ ))) = (a * ((A * B) @ )) by A1, A4, MATRIX_3: 22;

      

       A6: ( width (a * (A * B))) = ( width (A * B)) by Th27

      .= ( width B) by A1, MATRIX_3:def 4;

      

       A7: ( len (a * (A * B))) = ( len (A * B)) by Th27

      .= ( len A) by A1, MATRIX_3:def 4;

      

       A8: ( len (a * A)) = ( len A) by Th27;

      

       A9: ( width (a * A)) = ( width A) by Th27;

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

      then ((B @ ) * (a * (A @ ))) = ((a * (A * B)) @ ) by A4, A5, Th30;

      then ((B @ ) * ((a * A) @ )) = ((a * (A * B)) @ ) by A1, A3, Th30;

      then

       A10: (((a * A) * B) @ ) = ((a * (A * B)) @ ) by A1, A4, A9, MATRIX_3: 22;

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

      then ((a * A) * B) = (((a * (A * B)) @ ) @ ) by A2, A4, A8, A10, MATRIX_0: 57;

      hence thesis by A2, A4, A7, A6, MATRIX_0: 57;

    end;

    theorem :: MATRIXR1:42

    for M be Matrix of REAL holds (M + ( 0_Rmatrix (( len M),( width M)))) = M

    proof

      let M be Matrix of REAL ;

      

       A1: ( len M) = ( len ( MXR2MXF M)) & ( width M) = ( width ( MXR2MXF M));

      (M + ( 0_Rmatrix (( len M),( width M)))) = (M + ( - ( 0_Rmatrix (( len M),( width M))))) by MATRIX_4: 9

      .= (M + ( - (M - M))) by MATRIX_4: 3

      .= ( MXF2MXR (( MXR2MXF M) - (( MXR2MXF M) - ( MXR2MXF M)))) by MATRIX_4:def 1

      .= M by A1, MATRIX_4: 11;

      hence thesis;

    end;

    theorem :: MATRIXR1:43

    for a be Real, A,B be Matrix of REAL st ( len A) = ( len B) & ( width A) = ( width B) holds (a * (A + B)) = ((a * A) + (a * B))

    proof

      let a be Real, A,B be Matrix of REAL ;

      assume

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

      reconsider ea = a as Element of F_Real by XREAL_0:def 1;

      

       A2: ((a * A) + (a * B)) = ( MXF2MXR (( MXR2MXF ( MXF2MXR (ea * ( MXR2MXF A)))) + ( MXR2MXF (a * B)))) by Def7

      .= ( MXF2MXR ((ea * ( MXR2MXF A)) + ( MXR2MXF ( MXF2MXR (ea * ( MXR2MXF B)))))) by Def7

      .= ( MXF2MXR ((ea * ( MXR2MXF A)) + (ea * ( MXR2MXF B))));

      (a * (A + B)) = ( MXF2MXR (ea * ( MXR2MXF (A + B)))) by Def7

      .= ( MXF2MXR ((ea * ( MXR2MXF A)) + (ea * ( MXR2MXF B)))) by A1, MATRIX_5: 20;

      hence thesis by A2;

    end;

    theorem :: MATRIXR1:44

    for A be Matrix of REAL st ( len A) > 0 holds ( 0 * A) = ( 0_Rmatrix (( len A),( width A)))

    proof

      let A be Matrix of REAL ;

      assume

       A1: ( len A) > 0 ;

      ( 0 * A) = ( MXF2MXR (( 0. F_Real ) * ( MXR2MXF A))) by Def7

      .= ( 0_Rmatrix (( len A),( width A))) by A1, MATRIX_5: 24;

      hence thesis;

    end;

    definition

      let x be FinSequence of REAL ;

      assume

       A1: ( len x) > 0 ;

      :: MATRIXR1:def9

      func ColVec2Mx x -> Matrix of REAL means

      : Def9: ( len it ) = ( len x) & ( width it ) = 1 & for j st j in ( dom x) holds (it . j) = <*(x . j)*>;

      existence

      proof

        reconsider n = ( len x) as Element of NAT ;

        deffunc F( Nat) = <*(x . $1)*>;

        consider C be FinSequence such that

         A2: ( len C) = n & for j be Nat st j in ( dom C) holds (C . j) = F(j) from FINSEQ_1:sch 2;

        for y be object st y in ( rng C) holds ex p be FinSequence of REAL st y = p & ( len p) = 1

        proof

          let y be object;

          assume y in ( rng C);

          then

          consider z be object such that

           A3: z in ( dom C) and

           A4: y = (C . z) by FUNCT_1:def 3;

          reconsider z as Element of NAT by A3;

          reconsider xz = (x . z) as Element of REAL by XREAL_0:def 1;

          ( len <*xz*>) = 1 by FINSEQ_1: 39;

          hence thesis by A2, A3, A4;

        end;

        then

        reconsider B = C as Matrix of REAL by MATRIX_0: 9;

        for p be FinSequence of REAL st p in ( rng B) holds ( len p) = 1

        proof

          let p be FinSequence of REAL ;

          assume p in ( rng B);

          then

          consider i be Nat such that

           A5: i in ( dom B) & (B . i) = p by FINSEQ_2: 10;

          ( len <*(x . i)*>) = 1 by FINSEQ_1: 39;

          hence thesis by A2, A5;

        end;

        then

        reconsider A = B as Matrix of ( len B), 1, REAL by MATRIX_0:def 2;

        

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

        ( dom C) = ( Seg n) & ( width A) = 1 by A1, A2, FINSEQ_1:def 3, MATRIX_0: 23;

        hence thesis by A2, A6;

      end;

      uniqueness

      proof

        let A,B be Matrix of REAL ;

        assume that

         A7: ( len A) = ( len x) and ( width A) = 1 and

         A8: for k be Nat st k in ( dom x) holds (A . k) = <*(x . k)*> and

         A9: ( len B) = ( len x) and ( width B) = 1 and

         A10: for k be Nat st k in ( dom x) holds (B . k) = <*(x . k)*>;

         A11:

        now

          let k be Nat;

          assume

           A12: k in ( dom x);

          

          hence (A . k) = <*(x . k)*> by A8

          .= (B . k) by A10, A12;

        end;

        ( dom A) = ( dom x) & ( dom B) = ( dom x) by A7, A9, FINSEQ_3: 29;

        hence thesis by A11, FINSEQ_1: 13;

      end;

    end

    theorem :: MATRIXR1:45

    for x be FinSequence of REAL , M be Matrix of REAL st ( len x) > 0 holds M = ( ColVec2Mx x) iff ( Col (M,1)) = x & ( width M) = 1

    proof

      let x be FinSequence of REAL , M be Matrix of REAL ;

      consider n be Nat such that

       A1: for x be object st x in ( rng M) holds ex s2 be FinSequence st s2 = x & ( len s2) = n by MATRIX_0:def 1;

      assume

       A2: ( len x) > 0 ;

      thus M = ( ColVec2Mx x) implies ( Col (M,1)) = x & ( width M) = 1

      proof

        assume

         A3: M = ( ColVec2Mx x);

        then

         A4: ( width M) = 1 by A2, Def9;

        

         A5: ( len M) = ( len x) by A2, A3, Def9;

        then

         A6: ( dom M) = ( dom x) by FINSEQ_3: 29;

        for j st j in ( dom M) holds (x . j) = (M * (j,1))

        proof

          let j;

          reconsider xj = (x . j) as Element of REAL by XREAL_0:def 1;

          assume

           A7: j in ( dom M);

          then

          reconsider j as Element of NAT ;

          

           A8: (M . j) = <*xj*> by A2, A3, A6, A7, Def9;

          then

          reconsider q = (M . j) as FinSequence of REAL ;

          

           A9: (q . 1) = xj by A8, FINSEQ_1: 40;

          1 in ( Seg ( width M)) by A4, FINSEQ_1: 1;

          then [j, 1] in ( Indices M) by A7, ZFMISC_1: 87;

          hence thesis by A9, MATRIX_0:def 5;

        end;

        hence thesis by A2, A3, A5, Def9, MATRIX_0:def 8;

      end;

      assume that

       A10: ( Col (M,1)) = x and

       A11: ( width M) = 1;

      

       A12: ( len x) = ( len M) by A10, MATRIX_0:def 8;

      then

      consider s be FinSequence such that

       A13: s in ( rng M) and

       A14: ( len s) = 1 by A2, A11, MATRIX_0:def 3;

      

       A15: ( dom x) = ( dom M) by A12, FINSEQ_3: 29;

      

       A16: ex s2 be FinSequence st s2 = s & ( len s2) = n by A13, A1;

      for j st j in ( dom x) holds (M . j) = <*(x . j)*>

      proof

        let j;

        assume

         A17: j in ( dom x);

        then (M . j) in ( rng M) by A15, FUNCT_1:def 3;

        then

         A18: ex s3 be FinSequence st s3 = (M . j) & ( len s3) = 1 by A14, A1, A16;

        1 in ( Seg ( width M)) by A11, FINSEQ_1: 1;

        then [j, 1] in ( Indices M) by A15, A17, ZFMISC_1: 87;

        then

         A19: ex p be FinSequence of REAL st p = (M . j) & (M * (j,1)) = (p . 1) by MATRIX_0:def 5;

        (x . j) = (M * (j,1)) by A10, A15, A17, MATRIX_0:def 8;

        hence thesis by A19, A18, FINSEQ_1: 40;

      end;

      hence thesis by A2, A11, A12, Def9;

    end;

    theorem :: MATRIXR1:46

    

     Th46: for x1,x2 be FinSequence of REAL st ( len x1) = ( len x2) & ( len x1) > 0 holds ( ColVec2Mx (x1 + x2)) = (( ColVec2Mx x1) + ( ColVec2Mx x2))

    proof

      let x1,x2 be FinSequence of REAL ;

      assume that

       A1: ( len x1) = ( len x2) and

       A2: ( len x1) > 0 ;

      

       A3: ( width ( ColVec2Mx x1)) = 1 by A2, Def9;

      

       A4: ( Seg ( width ( ColVec2Mx x1))) = ( Seg 1) by A2, Def9;

      

       A5: ( dom x1) = ( dom x2) by A1, FINSEQ_3: 29;

      

       A6: ( len ( ColVec2Mx x1)) = ( len x1) by A2, Def9;

      then

       A7: ( dom ( ColVec2Mx x1)) = ( dom x1) by FINSEQ_3: 29;

      ( len ( ColVec2Mx x2)) = ( len x2) & ( width ( ColVec2Mx x2)) = 1 by A1, A2, Def9;

      then

       A8: ( Indices ( ColVec2Mx x2)) = ( Indices ( ColVec2Mx x1)) by A1, A6, A3, MATRIX_4: 55;

      

       A9: ( len (x1 + x2)) = ( len x1) by A1, RVSUM_1: 115;

      then

       A10: ( dom (x1 + x2)) = ( dom x1) by FINSEQ_3: 29;

      

       A11: ( len ( ColVec2Mx (x1 + x2))) = ( len (x1 + x2)) & ( width ( ColVec2Mx (x1 + x2))) = 1 by A2, A9, Def9;

      then

       A12: ( Indices ( ColVec2Mx (x1 + x2))) = ( Indices ( ColVec2Mx x1)) by A1, A6, A3, MATRIX_4: 55, RVSUM_1: 115;

      for i, j st [i, j] in ( Indices ( ColVec2Mx x1)) holds (( ColVec2Mx (x1 + x2)) * (i,j)) = ((( ColVec2Mx x1) * (i,j)) + (( ColVec2Mx x2) * (i,j)))

      proof

        let i, j;

        thus [i, j] in ( Indices ( ColVec2Mx x1)) implies (( ColVec2Mx (x1 + x2)) * (i,j)) = ((( ColVec2Mx x1) * (i,j)) + (( ColVec2Mx x2) * (i,j)))

        proof

          assume

           A13: [i, j] in ( Indices ( ColVec2Mx x1));

          then

          consider q1 be FinSequence of REAL such that

           A14: q1 = (( ColVec2Mx x1) . i) and

           A15: (( ColVec2Mx x1) * (i,j)) = (q1 . j) by MATRIX_0:def 5;

          j in ( Seg 1) by A4, A13, ZFMISC_1: 87;

          then 1 <= j & j <= 1 by FINSEQ_1: 1;

          then

           A16: j = 1 by XXREAL_0: 1;

          

           A17: i in ( dom x1) by A7, A13, ZFMISC_1: 87;

          then (( ColVec2Mx x1) . i) = <*(x1 . i)*> by A2, Def9;

          then

           A18: (q1 . j) = (x1 . i) by A16, A14, FINSEQ_1: 40;

          consider p be FinSequence of REAL such that

           A19: p = (( ColVec2Mx (x1 + x2)) . i) and

           A20: (( ColVec2Mx (x1 + x2)) * (i,j)) = (p . j) by A12, A13, MATRIX_0:def 5;

          consider q2 be FinSequence of REAL such that

           A21: q2 = (( ColVec2Mx x2) . i) and

           A22: (( ColVec2Mx x2) * (i,j)) = (q2 . j) by A8, A13, MATRIX_0:def 5;

          (( ColVec2Mx x2) . i) = <*(x2 . i)*> by A1, A2, A5, A17, Def9;

          then

           A23: (q2 . j) = (x2 . i) by A16, A21, FINSEQ_1: 40;

          (( ColVec2Mx (x1 + x2)) . i) = <*((x1 + x2) . i)*> by A2, A9, A10, A17, Def9;

          then (p . j) = ((x1 + x2) . i) by A16, A19, FINSEQ_1: 40;

          hence thesis by A10, A17, A20, A15, A18, A22, A23, VALUED_1:def 1;

        end;

      end;

      hence thesis by A1, A6, A11, A3, Th26, RVSUM_1: 115;

    end;

    theorem :: MATRIXR1:47

    

     Th47: for a be Real, x be FinSequence of REAL st ( len x) > 0 holds ( ColVec2Mx (a * x)) = (a * ( ColVec2Mx x))

    proof

      let a be Real, x be FinSequence of REAL ;

      assume

       A1: ( len x) > 0 ;

      

       A2: ( len (a * ( ColVec2Mx x))) = ( len ( ColVec2Mx x)) by Th27

      .= ( len x) by A1, Def9;

      

       A3: ( len (a * x)) = ( len x) by RVSUM_1: 117;

      then

       A4: ( dom (a * x)) = ( dom x) by FINSEQ_3: 29;

      

       A5: for j st j in ( dom (a * x)) holds ((a * ( ColVec2Mx x)) . j) = <*((a * x) . j)*>

      proof

        ( len ( ColVec2Mx x)) = ( len x) by A1, Def9;

        then

         A6: ( dom ( ColVec2Mx x)) = ( dom x) by FINSEQ_3: 29;

        let j;

        consider n be Nat such that

         A7: for x2 be object st x2 in ( rng (a * ( ColVec2Mx x))) holds ex s2 be FinSequence st s2 = x2 & ( len s2) = n by MATRIX_0:def 1;

        assume

         A8: j in ( dom (a * x));

        then

         A9: (( ColVec2Mx x) . j) = <*(x . j)*> by A1, A4, Def9;

        

         A10: j in ( dom (a * ( ColVec2Mx x))) by A2, A3, A8, FINSEQ_3: 29;

        then ((a * ( ColVec2Mx x)) . j) in ( rng (a * ( ColVec2Mx x))) by FUNCT_1:def 3;

        then

        reconsider q = ((a * ( ColVec2Mx x)) . j) as FinSequence of REAL by FINSEQ_1:def 11;

        q in ( rng (a * ( ColVec2Mx x))) by A10, FUNCT_1:def 3;

        then

         A11: ex s2 be FinSequence st s2 = q & ( len s2) = n by A7;

        consider s be FinSequence such that

         A12: s in ( rng (a * ( ColVec2Mx x))) and

         A13: ( len s) = ( width (a * ( ColVec2Mx x))) by A1, A2, MATRIX_0:def 3;

        ex s3 be FinSequence st s3 = s & ( len s3) = n by A12, A7;

        

        then

         A14: ( len q) = ( width ( ColVec2Mx x)) by A13, A11, Th27

        .= 1 by A1, Def9

        .= ( len <*((a * x) . j)*>) by FINSEQ_1: 40;

        ( width ( ColVec2Mx x)) = 1 by A1, Def9;

        then

         A15: 1 in ( Seg ( width ( MXR2MXF ( ColVec2Mx x)))) by FINSEQ_1: 1;

        j in ( dom x) by A3, A8, FINSEQ_3: 29;

        then

         A16: [j, 1] in ( Indices ( MXR2MXF ( ColVec2Mx x))) by A6, A15, ZFMISC_1: 87;

        then

         A17: ex p3 be FinSequence of REAL st p3 = (( ColVec2Mx x) . j) & (( ColVec2Mx x) * (j,1)) = (p3 . 1) by MATRIX_0:def 5;

         [j, 1] in ( Indices (a * ( ColVec2Mx x))) by A16, Th28;

        then

         A18: ex p be FinSequence of REAL st p = ((a * ( ColVec2Mx x)) . j) & ((a * ( ColVec2Mx x)) * (j,1)) = (p . 1) by MATRIX_0:def 5;

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

        

         A19: (q . 1) = (a * (( ColVec2Mx x) * (j,1))) by A16, A18, Th29

        .= (a * (x . j)) by A17, A9, FINSEQ_1: 40

        .= ((a * x) . j) by RVSUM_1: 44

        .= ( <*((a * x) . j)*> . 1) by FINSEQ_1: 40;

        for i be Nat st 1 <= i & i <= ( len <*((a * x) . j)*>) holds (q . i) = ( <*((a * x) . j)*> . i)

        proof

          let i be Nat;

          

           A20: ( len <*((a * x) . j)*>) = 1 by FINSEQ_1: 40;

          assume 1 <= i & i <= ( len <*((a * x) . j)*>);

          then i = 1 by A20, XXREAL_0: 1;

          hence thesis by A19;

        end;

        hence thesis by A14, FINSEQ_1: 14;

      end;

      ( width (a * ( ColVec2Mx x))) = ( width ( ColVec2Mx x)) by Th27

      .= 1 by A1, Def9;

      hence thesis by A1, A2, A3, A5, Def9;

    end;

    definition

      let x be FinSequence of REAL ;

      :: MATRIXR1:def10

      func LineVec2Mx x -> Matrix of REAL means

      : Def10: ( width it ) = ( len x) & ( len it ) = 1 & for j st j in ( dom x) holds (it * (1,j)) = (x . j);

      existence

      proof

        set B = <*x*>;

        

         A1: ( rng B) = {x} by FINSEQ_1: 39;

        for y be object st y in ( rng B) holds ex p be FinSequence of REAL st y = p & ( len p) = ( len x)

        proof

          let y be object;

          assume y in ( rng B);

          then y = x by A1, TARSKI:def 1;

          hence thesis;

        end;

        then

        reconsider C = B as Matrix of REAL by MATRIX_0: 9;

        take C;

        

         A2: ( len B) = 1 by FINSEQ_1: 39;

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

        then

         A3: 1 in ( dom C) by FINSEQ_1: 1;

        for p be FinSequence of REAL st p in ( rng C) holds ( len p) = ( len x) by A1, TARSKI:def 1;

        then ( len B) = 1 & C is Matrix of 1, ( len x), REAL by A2, MATRIX_0:def 2;

        hence

         A4: ( width C) = ( len x) by MATRIX_0: 20;

        thus ( len C) = 1 by FINSEQ_1: 40;

        let j be Nat;

        

         A5: (x . j) in REAL by XREAL_0:def 1;

        assume j in ( dom x);

        then j in ( Seg ( len x)) by FINSEQ_1:def 3;

        then (B . 1) = x & [1, j] in ( Indices C) by A4, A3, FINSEQ_1: 40, ZFMISC_1:def 2;

        hence thesis by MATRIX_0:def 5, A5;

      end;

      uniqueness

      proof

        let A,B be Matrix of REAL ;

        assume that

         A6: ( width A) = ( len x) and

         A7: ( len A) = 1 and

         A8: for k be Nat st k in ( dom x) holds (A * (1,k)) = (x . k) and

         A9: ( width B) = ( len x) & ( len B) = 1 and

         A10: for k be Nat st k in ( dom x) holds (B * (1,k)) = (x . k);

        

         A11: ( dom A) = ( Seg 1) by A7, FINSEQ_1:def 3;

        for i, j st [i, j] in ( Indices A) holds (A * (i,j)) = (B * (i,j))

        proof

          let i, j;

          assume

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

          then i in ( Seg 1) by A11, ZFMISC_1: 87;

          then 1 <= i & i <= 1 by FINSEQ_1: 1;

          then

           A13: i = 1 by XXREAL_0: 1;

          j in ( Seg ( len x)) by A6, A12, ZFMISC_1: 87;

          then

           A14: j in ( dom x) by FINSEQ_1:def 3;

          then (A * (i,j)) = (x . j) by A8, A13;

          hence thesis by A10, A14, A13;

        end;

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

      end;

    end

    theorem :: MATRIXR1:48

    for x be FinSequence of REAL , M be Matrix of REAL holds M = ( LineVec2Mx x) iff ( Line (M,1)) = x & ( len M) = 1

    proof

      let x be FinSequence of REAL , M be Matrix of REAL ;

      thus M = ( LineVec2Mx x) implies ( Line (M,1)) = x & ( len M) = 1

      proof

        assume

         A1: M = ( LineVec2Mx x);

        then

         A2: for j st j in ( dom x) holds (M * (1,j)) = (x . j) by Def10;

        

         A3: ( width M) = ( len x) by A1, Def10;

        then ( dom x) = ( Seg ( width M)) by FINSEQ_1:def 3;

        hence thesis by A1, A3, A2, Def10, MATRIX_0:def 7;

      end;

      assume that

       A4: ( Line (M,1)) = x and

       A5: ( len M) = 1;

      

       A6: for j st j in ( Seg ( width M)) holds (x . j) = (M * (1,j)) by A4, MATRIX_0:def 7;

      

       A7: ( len x) = ( width M) by A4, MATRIX_0:def 7;

      then ( Seg ( width M)) = ( dom x) by FINSEQ_1:def 3;

      hence thesis by A5, A7, A6, Def10;

    end;

    theorem :: MATRIXR1:49

    

     Th49: for x be FinSequence of REAL st ( len x) > 0 holds (( LineVec2Mx x) @ ) = ( ColVec2Mx x) & (( ColVec2Mx x) @ ) = ( LineVec2Mx x)

    proof

      let x be FinSequence of REAL ;

      

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

      

       A2: ( width ( LineVec2Mx x)) = ( len x) by Def10;

      assume

       A3: ( len x) > 0 ;

      then

       A4: ( len ( ColVec2Mx x)) = ( len x) by Def9;

      

       A5: ( len ( LineVec2Mx x)) = 1 by Def10;

      

       A6: ( width ( ColVec2Mx x)) = 1 by A3, Def9;

      

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

      

       A8: for i, j holds [i, j] in ( Indices ( ColVec2Mx x)) iff [j, i] in ( Indices ( LineVec2Mx x))

      proof

        let i, j;

         [i, j] in ( Indices ( ColVec2Mx x)) iff i in ( dom ( ColVec2Mx x)) & j in ( Seg ( width ( ColVec2Mx x))) by ZFMISC_1: 87;

        hence thesis by A2, A5, A4, A6, A7, A1, ZFMISC_1: 87;

      end;

      

       A9: for i, j st [j, i] in ( Indices ( LineVec2Mx x)) holds (( ColVec2Mx x) * (i,j)) = (( LineVec2Mx x) * (j,i))

      proof

        let i, j;

        assume

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

        then [i, j] in ( Indices ( ColVec2Mx x)) by A8;

        then

         A11: ex p be FinSequence of REAL st p = (( ColVec2Mx x) . i) & (( ColVec2Mx x) * (i,j)) = (p . j) by MATRIX_0:def 5;

        j in ( Seg 1) by A5, A1, A10, ZFMISC_1: 87;

        then 1 <= j & j <= 1 by FINSEQ_1: 1;

        then

         A12: j = 1 by XXREAL_0: 1;

        i in ( Seg ( len x)) by A2, A10, ZFMISC_1: 87;

        then

         A13: i in ( dom x) by FINSEQ_1:def 3;

        then (( ColVec2Mx x) . i) = <*(x . i)*> by A3, Def9;

        

        hence (( ColVec2Mx x) * (i,j)) = (x . i) by A12, A11, FINSEQ_1: 40

        .= (( LineVec2Mx x) * (j,i)) by A12, A13, Def10;

      end;

      hence (( LineVec2Mx x) @ ) = ( ColVec2Mx x) by A2, A4, A8, MATRIX_0:def 6;

      

       A14: for i, j st [j, i] in ( Indices ( ColVec2Mx x)) holds (( LineVec2Mx x) * (i,j)) = (( ColVec2Mx x) * (j,i))

      proof

        let i, j;

        assume [j, i] in ( Indices ( ColVec2Mx x));

        then [i, j] in ( Indices ( LineVec2Mx x)) by A8;

        hence thesis by A9;

      end;

      for i, j holds [i, j] in ( Indices ( LineVec2Mx x)) iff [j, i] in ( Indices ( ColVec2Mx x)) by A8;

      hence thesis by A5, A6, A14, MATRIX_0:def 6;

    end;

    theorem :: MATRIXR1:50

    

     Th50: for x1,x2 be FinSequence of REAL st ( len x1) = ( len x2) holds ( LineVec2Mx (x1 + x2)) = (( LineVec2Mx x1) + ( LineVec2Mx x2))

    proof

      let x1,x2 be FinSequence of REAL ;

      assume

       A1: ( len x1) = ( len x2);

      then

       A2: ( dom x1) = ( dom x2) by FINSEQ_3: 29;

      ( len (x1 + x2)) = ( len x1) by A1, RVSUM_1: 115;

      then

       A3: ( dom (x1 + x2)) = ( dom x1) by FINSEQ_3: 29;

      

       A4: ( width ( LineVec2Mx x1)) = ( len x1) & ( len ( LineVec2Mx x1)) = 1 by Def10;

      ( width ( LineVec2Mx x2)) = ( len x2) & ( len ( LineVec2Mx x2)) = 1 by Def10;

      then

       A5: ( Indices ( LineVec2Mx x2)) = ( Indices ( LineVec2Mx x1)) by A1, A4, MATRIX_4: 55;

      

       A6: ( Seg ( width ( LineVec2Mx x1))) = ( Seg ( len x1)) by Def10

      .= ( dom x1) by FINSEQ_1:def 3;

      

       A7: ( dom ( LineVec2Mx x1)) = ( Seg ( len ( LineVec2Mx x1))) by FINSEQ_1:def 3

      .= ( Seg 1) by Def10;

      

       A8: ( width ( LineVec2Mx (x1 + x2))) = ( len (x1 + x2)) & ( len ( LineVec2Mx (x1 + x2))) = 1 by Def10;

      then

       A9: ( Indices ( LineVec2Mx (x1 + x2))) = ( Indices ( LineVec2Mx x1)) by A1, A4, MATRIX_4: 55, RVSUM_1: 115;

      for i, j holds [i, j] in ( Indices ( LineVec2Mx x1)) implies (( LineVec2Mx (x1 + x2)) * (i,j)) = ((( LineVec2Mx x1) * (i,j)) + (( LineVec2Mx x2) * (i,j)))

      proof

        let i, j;

        assume

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

        then

        consider q1 be FinSequence of REAL such that q1 = (( LineVec2Mx x1) . i) and

         A11: (( LineVec2Mx x1) * (i,j)) = (q1 . j) by MATRIX_0:def 5;

        consider p be FinSequence of REAL such that p = (( LineVec2Mx (x1 + x2)) . i) and

         A12: (( LineVec2Mx (x1 + x2)) * (i,j)) = (p . j) by A9, A10, MATRIX_0:def 5;

        consider q2 be FinSequence of REAL such that q2 = (( LineVec2Mx x2) . i) and

         A13: (( LineVec2Mx x2) * (i,j)) = (q2 . j) by A5, A10, MATRIX_0:def 5;

        

         A14: j in ( dom x1) by A6, A10, ZFMISC_1: 87;

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

        then 1 <= i & i <= 1 by FINSEQ_1: 1;

        then

         A15: i = 1 by XXREAL_0: 1;

        then

         A16: (q1 . j) = (x1 . j) by A14, A11, Def10;

        

         A17: (q2 . j) = (x2 . j) by A2, A14, A15, A13, Def10;

        (p . j) = ((x1 + x2) . j) by A3, A14, A15, A12, Def10;

        hence thesis by A3, A14, A12, A11, A16, A13, A17, VALUED_1:def 1;

      end;

      hence thesis by A1, A8, A4, Th26, RVSUM_1: 115;

    end;

    theorem :: MATRIXR1:51

    for a be Real, x be FinSequence of REAL holds ( LineVec2Mx (a * x)) = (a * ( LineVec2Mx x))

    proof

      let a be Real, x be FinSequence of REAL ;

      

       A1: ( len (a * ( LineVec2Mx x))) = ( len ( LineVec2Mx x)) by Th27

      .= 1 by Def10;

      

       A2: ( len (a * x)) = ( len x) by RVSUM_1: 117;

      then

       A3: ( dom (a * x)) = ( dom x) by FINSEQ_3: 29;

      

       A4: for j st j in ( dom (a * x)) holds ((a * ( LineVec2Mx x)) * (1,j)) = ((a * x) . j)

      proof

        ( len ( LineVec2Mx x)) = 1 by Def10;

        then 1 in ( Seg ( len ( LineVec2Mx x))) by FINSEQ_1: 1;

        then

         A5: 1 in ( dom ( LineVec2Mx x)) by FINSEQ_1:def 3;

        1 in ( Seg ( len (a * ( LineVec2Mx x)))) by A1, FINSEQ_1: 1;

        then 1 in ( dom (a * ( LineVec2Mx x))) by FINSEQ_1:def 3;

        then ((a * ( LineVec2Mx x)) . 1) in ( rng (a * ( LineVec2Mx x))) by FUNCT_1:def 3;

        then

        reconsider q = ((a * ( LineVec2Mx x)) . 1) as FinSequence of REAL by FINSEQ_1:def 11;

        let j;

        

         A6: ( width ( LineVec2Mx x)) = ( len x) by Def10;

        

         A7: ( Indices (a * ( LineVec2Mx x))) = ( Indices ( LineVec2Mx x)) by Th28;

        assume

         A8: j in ( dom (a * x));

        then j in ( Seg ( len x)) by A2, FINSEQ_1:def 3;

        then

         A9: [1, j] in ( Indices (a * ( LineVec2Mx x))) by A6, A5, A7, ZFMISC_1: 87;

        then

         A10: ex p be FinSequence of REAL st p = ((a * ( LineVec2Mx x)) . 1) & ((a * ( LineVec2Mx x)) * (1,j)) = (p . j) by MATRIX_0:def 5;

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

        

         A11: (q . j) in REAL by XREAL_0:def 1;

        (q . j) = (a * (( LineVec2Mx x) * (1,j))) by A7, A9, A10, Th29

        .= (a * (x . j)) by A3, A8, Def10

        .= ((a * x) . j) by RVSUM_1: 44;

        hence thesis by A9, MATRIX_0:def 5, A11;

      end;

      ( width (a * ( LineVec2Mx x))) = ( width ( LineVec2Mx x)) by Th27

      .= ( len x) by Def10;

      hence thesis by A1, A2, A4, Def10;

    end;

    definition

      let M be Matrix of REAL ;

      let x be FinSequence of REAL ;

      :: MATRIXR1:def11

      func M * x -> FinSequence of REAL equals ( Col ((M * ( ColVec2Mx x)),1));

      coherence ;

      :: MATRIXR1:def12

      func x * M -> FinSequence of REAL equals ( Line ((( LineVec2Mx x) * M),1));

      coherence ;

    end

    theorem :: MATRIXR1:52

    

     Th52: for x be FinSequence of REAL , A be Matrix of REAL st ( len A) > 0 & ( width A) > 0 & (( len A) = ( len x) or ( width (A @ )) = ( len x)) holds ((A @ ) * x) = (x * A)

    proof

      let x be FinSequence of REAL , A be Matrix of REAL ;

      assume that

       A1: ( len A) > 0 and

       A2: ( width A) > 0 and

       A3: ( len A) = ( len x) or ( width (A @ )) = ( len x);

      

       A4: ( len A) = ( len x) by A2, A3, MATRIX_0: 54;

      

       A5: ( len A) = ( width (A @ )) by A2, MATRIX_0: 54;

      then ( len ( ColVec2Mx x)) = ( len x) by A1, A3, Def9;

      then

       A6: ( width ((A @ ) * ( ColVec2Mx x))) = ( width ( ColVec2Mx x)) by A3, A5, MATRIX_3:def 4;

      ( width ( ColVec2Mx x)) = 1 by A1, A3, A5, Def9;

      then

       A7: 1 in ( Seg ( width ((A @ ) * ( ColVec2Mx x)))) by A6, FINSEQ_1: 1;

      

       A8: ( len ( LineVec2Mx x)) = 1 by Def10;

      

       A9: ( width ( LineVec2Mx x)) = ( len x) by Def10;

      then ( width ( LineVec2Mx x)) = ( len A) by A2, A3, MATRIX_0: 54;

      then ( len (( LineVec2Mx x) * A)) = ( len ( LineVec2Mx x)) & ( width (( LineVec2Mx x) * A)) = ( width A) by MATRIX_3:def 4;

      

      then ( Line ((( LineVec2Mx x) * A),1)) = ( Line ((((( LineVec2Mx x) * A) @ ) @ ),1)) by A2, A8, MATRIX_0: 57

      .= ( Line ((((A @ ) * (( LineVec2Mx x) @ )) @ ),1)) by A2, A4, A9, MATRIX_3: 22

      .= ( Line ((((A @ ) * ( ColVec2Mx x)) @ ),1)) by A1, A4, Th49

      .= ( Col (((A @ ) * ( ColVec2Mx x)),1)) by A7, MATRIX_0: 59;

      hence thesis;

    end;

    theorem :: MATRIXR1:53

    

     Th53: for x be FinSequence of REAL , A be Matrix of REAL st ( len A) > 0 & ( width A) > 0 & (( width A) = ( len x) or ( len (A @ )) = ( len x)) holds (A * x) = (x * (A @ ))

    proof

      let x be FinSequence of REAL , A be Matrix of REAL ;

      assume that

       A1: ( len A) > 0 and

       A2: ( width A) > 0 and

       A3: ( width A) = ( len x) or ( len (A @ )) = ( len x);

      ( len (A @ )) = ( width A) & ( width (A @ )) = ( len A) by A2, MATRIX_0: 54;

      then (((A @ ) @ ) * x) = (x * (A @ )) by A1, A2, A3, Th52;

      hence thesis by A1, A2, MATRIX_0: 57;

    end;

    theorem :: MATRIXR1:54

    

     Th54: for A,B be Matrix of REAL st ( len A) = ( len B) holds for i be Nat st 1 <= i & i <= ( width A) holds ( Col ((A + B),i)) = (( Col (A,i)) + ( Col (B,i)))

    proof

      let A,B be Matrix of REAL ;

      assume

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

      then

       A2: ( dom A) = ( dom B) by FINSEQ_3: 29;

      let i be Nat;

      

       A3: ( len ( Col (A,i))) = ( len A) by MATRIX_0:def 8;

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

      then

       A4: ( len (( Col (A,i)) + ( Col (B,i)))) = ( len ( Col (A,i))) by A1, A3, RVSUM_1: 115;

      assume 1 <= i & i <= ( width A);

      then

       A5: i in ( Seg ( width A)) by FINSEQ_1: 1;

      

       A6: ( len (A + B)) = ( len A) by Th25;

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

      then

       A7: ( dom (( Col (A,i)) + ( Col (B,i)))) = ( dom (A + B)) by A3, A6, A4, FINSEQ_1:def 3;

      for j st j in ( dom (A + B)) holds ((( Col (A,i)) + ( Col (B,i))) . j) = ((A + B) * (j,i))

      proof

        let j;

        assume

         A8: j in ( dom (A + B));

        then j in ( Seg ( len (A + B))) by FINSEQ_1:def 3;

        then

         A9: j in ( dom A) by A6, FINSEQ_1:def 3;

        then

         A10: [j, i] in ( Indices A) by A5, ZFMISC_1: 87;

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

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

        then ((( Col (A,i)) . j) + (( Col (B,i)) . j)) = ((A + B) * (j,i)) by A10, Th25;

        hence thesis by A7, A8, VALUED_1:def 1;

      end;

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

    end;

    theorem :: MATRIXR1:55

    

     Th55: for A,B be Matrix of REAL st ( width A) = ( width B) holds for i be Nat st 1 <= i & i <= ( len A) holds ( Line ((A + B),i)) = (( Line (A,i)) + ( Line (B,i)))

    proof

      let A,B be Matrix of REAL ;

      assume

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

      let i be Nat;

      

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

      assume 1 <= i & i <= ( len A);

      then

       A3: i in ( dom A) by FINSEQ_3: 25;

      

       A4: ( width (A + B)) = ( width A) by Th25;

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

      then

       A5: ( len (( Line (A,i)) + ( Line (B,i)))) = ( len ( Line (A,i))) by A1, A2, RVSUM_1: 115;

      then

       A6: ( dom (( Line (A,i)) + ( Line (B,i)))) = ( Seg ( width A)) by A2, FINSEQ_1:def 3;

      for j st j in ( Seg ( width (A + B))) holds ((( Line (A,i)) + ( Line (B,i))) . j) = ((A + B) * (i,j))

      proof

        let j;

        assume

         A7: j in ( Seg ( width (A + B)));

        then

         A8: j in ( Seg ( width A)) by Th25;

        then

         A9: [i, j] in ( Indices A) & (( Line (A,i)) . j) = (A * (i,j)) by A3, MATRIX_0:def 7, ZFMISC_1: 87;

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

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

        then ((( Line (A,i)) . j) + (( Line (B,i)) . j)) = ((A + B) * (i,j)) by A9, Th25;

        hence thesis by A4, A6, A7, VALUED_1:def 1;

      end;

      hence thesis by A2, A4, A5, MATRIX_0:def 7;

    end;

    theorem :: MATRIXR1:56

    

     Th56: for a be Real, M be Matrix of REAL , i be Nat st 1 <= i & i <= ( width M) holds ( Col ((a * M),i)) = (a * ( Col (M,i)))

    proof

      let a be Real, M be Matrix of REAL ;

      reconsider ea = a as Element of F_Real by XREAL_0:def 1;

      let i be Nat;

      assume

       A1: 1 <= i & i <= ( width M);

      ( Col ((a * M),i)) = ( Col (( MXF2MXR (ea * ( MXR2MXF M))),i)) by Def7

      .= (ea * ( Col (( MXR2MXF M),i))) by A1, Th19;

      hence thesis by Th17;

    end;

    theorem :: MATRIXR1:57

    for x1,x2 be FinSequence of REAL , A be Matrix of REAL st ( len x1) = ( len x2) & ( width A) = ( len x1) & ( len x1) > 0 & ( len A) > 0 holds (A * (x1 + x2)) = ((A * x1) + (A * x2))

    proof

      let x1,x2 be FinSequence of REAL , A be Matrix of REAL ;

      assume that

       A1: ( len x1) = ( len x2) and

       A2: ( width A) = ( len x1) and

       A3: ( len x1) > 0 and

       A4: ( len A) > 0 ;

      

       A5: ( len ( ColVec2Mx x2)) = ( len x2) by A1, A3, Def9;

      

       A6: ( len ( ColVec2Mx x1)) = ( len x1) by A3, Def9;

      

      then

       A7: ( len (A * ( ColVec2Mx x1))) = ( len A) by A2, MATRIX_3:def 4

      .= ( len (A * ( ColVec2Mx x2))) by A1, A2, A5, MATRIX_3:def 4;

      

       A8: ( width ( ColVec2Mx x1)) = 1 by A3, Def9;

      then

       A9: 1 <= ( width (A * ( ColVec2Mx x1))) by A2, A6, MATRIX_3:def 4;

      

       A10: ( width ( ColVec2Mx x2)) = 1 by A1, A3, Def9;

      

      thus (A * (x1 + x2)) = ( Col ((A * (( ColVec2Mx x1) + ( ColVec2Mx x2))),1)) by A1, A3, Th46

      .= ( Col (((A * ( ColVec2Mx x1)) + (A * ( ColVec2Mx x2))),1)) by A1, A2, A3, A4, A6, A5, A8, A10, MATRIX_4: 62

      .= ((A * x1) + (A * x2)) by A7, A9, Th54;

    end;

    theorem :: MATRIXR1:58

    for x1,x2 be FinSequence of REAL , A be Matrix of REAL st ( len x1) = ( len x2) & ( len A) = ( len x1) & ( len x1) > 0 holds ((x1 + x2) * A) = ((x1 * A) + (x2 * A))

    proof

      let x1,x2 be FinSequence of REAL , A be Matrix of REAL ;

      assume that

       A1: ( len x1) = ( len x2) and

       A2: ( len A) = ( len x1) and

       A3: ( len x1) > 0 ;

      

       A4: ( width ( LineVec2Mx x2)) = ( len x2) by Def10;

      

       A5: ( width ( LineVec2Mx x1)) = ( len x1) by Def10;

      

      then

       A6: ( width (( LineVec2Mx x1) * A)) = ( width A) by A2, MATRIX_3:def 4

      .= ( width (( LineVec2Mx x2) * A)) by A1, A2, A4, MATRIX_3:def 4;

      

       A7: ( len ( LineVec2Mx x1)) = 1 by Def10;

      then

       A8: 1 <= ( len (( LineVec2Mx x1) * A)) by A2, A5, MATRIX_3:def 4;

      

       A9: ( len ( LineVec2Mx x2)) = 1 by Def10;

      

      thus ((x1 + x2) * A) = ( Line (((( LineVec2Mx x1) + ( LineVec2Mx x2)) * A),1)) by A1, Th50

      .= ( Line (((( LineVec2Mx x1) * A) + (( LineVec2Mx x2) * A)),1)) by A1, A2, A3, A5, A4, A7, A9, MATRIX_4: 63

      .= ((x1 * A) + (x2 * A)) by A6, A8, Th55;

    end;

    theorem :: MATRIXR1:59

    

     Th59: for a be Real, x be FinSequence of REAL , A be Matrix of REAL st ( width A) = ( len x) & ( len x) > 0 holds (A * (a * x)) = (a * (A * x))

    proof

      let a be Real, x be FinSequence of REAL , A be Matrix of REAL ;

      assume that

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

       A2: ( len x) > 0 ;

      

       A3: ( len ( ColVec2Mx x)) = ( len x) by A2, Def9;

      ( width ( ColVec2Mx x)) = 1 by A2, Def9;

      then

       A4: 1 <= ( width (A * ( ColVec2Mx x))) by A1, A3, MATRIX_3:def 4;

      

      thus (A * (a * x)) = ( Col ((A * (a * ( ColVec2Mx x))),1)) by A2, Th47

      .= ( Col ((a * (A * ( ColVec2Mx x))),1)) by A1, A3, Th40

      .= (a * (A * x)) by A4, Th56;

    end;

    theorem :: MATRIXR1:60

    for a be Real, x be FinSequence of REAL , A be Matrix of REAL st ( len A) = ( len x) & ( len x) > 0 & ( width A) > 0 holds ((a * x) * A) = (a * (x * A))

    proof

      let a be Real, x be FinSequence of REAL , A be Matrix of REAL ;

      assume that

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

       A2: ( len x) > 0 and

       A3: ( width A) > 0 ;

      

       A4: ((A @ ) * x) = (x * A) by A1, A2, A3, Th52;

      

       A5: ( width (A @ )) = ( len x) by A1, A3, MATRIX_0: 54;

      then

       A6: ((A @ ) * (a * x)) = (a * ((A @ ) * x)) by A2, Th59;

      

       A7: ( len (a * x)) = ( len x) by RVSUM_1: 117;

      ( len (A @ )) > 0 by A3, MATRIX_0: 54;

      then ((a * x) * ((A @ ) @ )) = ((A @ ) * (a * x)) by A2, A5, A7, Th53;

      hence thesis by A1, A2, A3, A6, A4, MATRIX_0: 57;

    end;

    theorem :: MATRIXR1:61

    

     Th61: for x be FinSequence of REAL , A be Matrix of REAL st ( width A) = ( len x) & ( len x) > 0 holds ( len (A * x)) = ( len A)

    proof

      let x be FinSequence of REAL , A be Matrix of REAL ;

      assume that

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

       A2: ( len x) > 0 ;

      

       A3: ( len ( ColVec2Mx x)) = ( len x) by A2, Def9;

      ( len ( Col ((A * ( ColVec2Mx x)),1))) = ( len (A * ( ColVec2Mx x))) by MATRIX_0:def 8

      .= ( len A) by A1, A3, MATRIX_3:def 4;

      hence thesis;

    end;

    theorem :: MATRIXR1:62

    

     Th62: for x be FinSequence of REAL , A be Matrix of REAL st ( len A) = ( len x) holds ( len (x * A)) = ( width A)

    proof

      let x be FinSequence of REAL , A be Matrix of REAL ;

      assume

       A1: ( len A) = ( len x);

      

       A2: ( width ( LineVec2Mx x)) = ( len x) by Def10;

      ( len ( Line ((( LineVec2Mx x) * A),1))) = ( width ( MXF2MXR (( MXR2MXF ( LineVec2Mx x)) * ( MXR2MXF A)))) by MATRIX_0:def 7

      .= ( width A) by A1, A2, MATRIX_3:def 4;

      hence thesis;

    end;

    theorem :: MATRIXR1:63

    

     Th63: for x be FinSequence of REAL , A,B be Matrix of REAL st ( len A) = ( len B) & ( width A) = ( width B) & ( width A) = ( len x) & ( len A) > 0 & ( len x) > 0 holds ((A + B) * x) = ((A * x) + (B * x))

    proof

      let x be FinSequence of REAL , A,B be Matrix of REAL ;

      assume that

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

       A2: ( width A) = ( len x) and

       A3: ( len A) > 0 and

       A4: ( len x) > 0 ;

      

       A5: ( len ( ColVec2Mx x)) = ( len x) by A4, Def9;

      

      then

       A6: ( len (A * ( ColVec2Mx x))) = ( len A) by A2, MATRIX_3:def 4

      .= ( len (B * ( ColVec2Mx x))) by A1, A2, A5, MATRIX_3:def 4;

      

       A7: ( width (A * ( ColVec2Mx x))) = ( width ( ColVec2Mx x)) by A2, A5, MATRIX_3:def 4

      .= 1 by A4, Def9;

      

      thus ((A + B) * x) = ( Col (((A * ( ColVec2Mx x)) + (B * ( ColVec2Mx x))),1)) by A1, A2, A3, A4, A5, MATRIX_4: 63

      .= ((A * x) + (B * x)) by A6, A7, Th54;

    end;

    theorem :: MATRIXR1:64

    

     Th64: for x be FinSequence of REAL , A,B be Matrix of REAL st ( len A) = ( len B) & ( width A) = ( width B) & ( len A) = ( len x) & ( len x) > 0 holds (x * (A + B)) = ((x * A) + (x * B))

    proof

      let x be FinSequence of REAL , A,B be Matrix of REAL ;

      assume that

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

       A2: ( len A) = ( len x) and

       A3: ( len x) > 0 ;

      

       A4: ( width ( LineVec2Mx x)) = ( len x) by Def10;

      

      then

       A5: ( len (( LineVec2Mx x) * A)) = ( len ( LineVec2Mx x)) by A2, MATRIX_3:def 4

      .= 1 by Def10;

      

       A6: ( width (( LineVec2Mx x) * A)) = ( width A) by A2, A4, MATRIX_3:def 4

      .= ( width (( LineVec2Mx x) * B)) by A1, A2, A4, MATRIX_3:def 4;

      ( len ( LineVec2Mx x)) = 1 by Def10;

      

      hence (x * (A + B)) = ( Line (((( LineVec2Mx x) * A) + (( LineVec2Mx x) * B)),1)) by A1, A2, A3, A4, MATRIX_4: 62

      .= ((x * A) + (x * B)) by A6, A5, Th55;

    end;

    theorem :: MATRIXR1:65

    for n,m be Nat, x be FinSequence of REAL st ( len x) = m & n > 0 & m > 0 holds (( 0_Rmatrix (n,m)) * x) = ( 0* n)

    proof

      let n,m be Nat, x be FinSequence of REAL ;

      assume that

       A1: ( len x) = m and

       A2: n > 0 and

       A3: m > 0 ;

      

       A4: ( width ( 0_Rmatrix (n,m))) = m by A2, MATRIX_0: 23;

      then

       A5: ( len (( 0_Rmatrix (n,m)) * x)) = ( len ( 0_Rmatrix (n,m))) by A1, A3, Th61;

      

       A6: ( len ( 0_Rmatrix (n,m))) = n by A2, MATRIX_0: 23;

      

      then (( 0_Rmatrix (n,m)) * x) = ((( 0_Rmatrix (n,m)) + ( 0_Rmatrix (n,m))) * x) by A2, A4, Th36

      .= ((( 0_Rmatrix (n,m)) * x) + (( 0_Rmatrix (n,m)) * x)) by A1, A2, A3, A6, A4, Th63;

      then ( 0* n) = (((( 0_Rmatrix (n,m)) * x) + (( 0_Rmatrix (n,m)) * x)) - (( 0_Rmatrix (n,m)) * x)) by A6, A5, Th3;

      hence thesis by A5, Th14;

    end;

    theorem :: MATRIXR1:66

    for n,m be Nat, x be FinSequence of REAL st ( len x) = n & n > 0 holds (x * ( 0_Rmatrix (n,m))) = ( 0* m)

    proof

      let n,m be Nat, x be FinSequence of REAL ;

      assume that

       A1: ( len x) = n and

       A2: n > 0 ;

      

       A3: ( len ( 0_Rmatrix (n,m))) = n by A2, MATRIX_0: 23;

      then

       A4: ( len (x * ( 0_Rmatrix (n,m)))) = ( width ( 0_Rmatrix (n,m))) by A1, Th62;

      

       A5: ( width ( 0_Rmatrix (n,m))) = m by A2, MATRIX_0: 23;

      

      then (x * ( 0_Rmatrix (n,m))) = (x * (( 0_Rmatrix (n,m)) + ( 0_Rmatrix (n,m)))) by A2, A3, Th36

      .= ((x * ( 0_Rmatrix (n,m))) + (x * ( 0_Rmatrix (n,m)))) by A1, A2, A5, A3, Th64;

      then ( 0* m) = (((x * ( 0_Rmatrix (n,m))) + (x * ( 0_Rmatrix (n,m)))) - (x * ( 0_Rmatrix (n,m)))) by A5, A4, Th3;

      hence thesis by A4, Th14;

    end;