matrixr2.miz



    begin

    reserve x for set,

D for non empty set,

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

K for Field;

    

     Lm1: for F1,F2 be FinSequence of REAL , j st ( len F1) = ( len F2) holds ((F1 - F2) . j) = ((F1 . j) - (F2 . j))

    proof

      let F1,F2 be FinSequence of REAL , j;

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

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

      assume ( len F1) = ( len F2);

      then

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

      ((G1 - G2) . j) = ((G1 . j) - (G2 . j)) by RVSUM_1: 27;

      hence thesis;

    end;

    theorem :: MATRIXR2:1

    

     Th1: for x,y be FinSequence of REAL st ( len x) = ( len y) & (x + y) = ( 0* ( len x)) holds x = ( - y) & y = ( - x)

    proof

      let x,y be FinSequence of REAL ;

      assume that

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

       A2: (x + y) = ( 0* ( len x));

      

       A3: x = (( 0* ( len x)) - y) by A1, A2, MATRIXR1: 14;

      hence x = ( - y) by A1, MATRIXR1: 6;

      

      thus ( - x) = ( - ( - y)) by A1, A3, MATRIXR1: 6

      .= y;

    end;

    

     Lm2: for A be Matrix of D st 1 <= i & i <= ( len A) holds ( Line (A,i)) = (A . i)

    proof

      let A be Matrix of D;

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

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

      hence thesis by MATRIX_0: 60;

    end;

    theorem :: MATRIXR2:2

    

     Th2: for A be Matrix of D holds for p be FinSequence of D st p = (A . i) & 1 <= i & i <= ( len A) & 1 <= j & j <= ( width A) & ( len p) = ( width A) holds (A * (i,j)) = (p . j)

    proof

      let A be Matrix of D;

      let p be FinSequence of D;

      assume that

       A1: p = (A . i) and

       A2: 1 <= i & i <= ( len A) and

       A3: 1 <= j & j <= ( width A) and

       A4: ( len p) = ( width A);

      

       A5: j in ( Seg ( width A)) by A3;

      then j in ( dom p) by A4, FINSEQ_1:def 3;

      then ( rng p) c= D & (p . j) in ( rng p) by FINSEQ_1:def 4, FUNCT_1:def 3;

      then

      reconsider xp = (p . j) as Element of D;

      

       A6: xp = (p . j);

      i in ( dom A) by A2, FINSEQ_3: 25;

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

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

    end;

    theorem :: MATRIXR2:3

    

     Th3: for a be Real, A be Matrix of REAL st [i, j] in ( Indices A) holds ((a * A) * (i,j)) = (a * (A * (i,j)))

    proof

      let a be Real, A be Matrix of REAL ;

      assume

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

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

      ((a * A) * (i,j)) = (( MXF2MXR (aa * ( MXR2MXF A))) * (i,j)) by MATRIXR1:def 7

      .= (aa * (( MXR2MXF A) * (i,j))) by A1, MATRIX_3:def 5

      .= (a * (A * (i,j)));

      hence thesis;

    end;

    theorem :: MATRIXR2:4

    for A,B be Matrix of n, REAL holds ( len (A * B)) = ( len A) & ( width (A * B)) = ( width B) & ( len (A * B)) = n & ( width (A * B)) = n

    proof

      let A,B be Matrix of n, REAL ;

      

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

      

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

      per cases ;

        suppose

         A3: n > 0 ;

        

        then ( width ( MXR2MXF A)) = n by MATRIX_0: 23

        .= ( len ( MXR2MXF B)) by MATRIX_0: 25;

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

        hence thesis by A1, A3, MATRIX_0: 20, MATRIX_0: 25;

      end;

        suppose

         A4: n <= 0 ;

        

        then

         A5: ( width ( MXR2MXF A)) = 0 by A2, MATRIX_0:def 3

        .= ( len ( MXR2MXF B)) by A4, MATRIX_0: 25;

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

        hence thesis by A2, A4, A5, MATRIX_0:def 3, MATRIX_3:def 4;

      end;

    end;

    theorem :: MATRIXR2:5

    

     Th5: 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;

      

       A1: ( width (a * A)) = ( width ( MXR2MXF ( MXF2MXR (ea * ( MXR2MXF A))))) by MATRIXR1:def 7

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

      ( len (a * A)) = ( len ( MXR2MXF ( MXF2MXR (ea * ( MXR2MXF A))))) by MATRIXR1:def 7

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

      hence thesis by A1;

    end;

    begin

    theorem :: MATRIXR2:6

    

     Th6: for A,B be Matrix of REAL st ( len A) = ( len B) & ( width A) = ( width B) 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 ;

      assume

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

      

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

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

      

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

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

      thus thesis by A1, MATRIX10: 3;

    end;

    definition

      let n;

      let A,B be Matrix of n, REAL ;

      :: original: *

      redefine

      func A * B -> Matrix of n, REAL ;

      coherence ;

    end

    theorem :: MATRIXR2:7

    

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

    proof

      let A,B be Matrix of REAL ;

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

      

      hence A = (A + ( 0_Rmatrix (( len B),( width B)))) by MATRIXR1: 36

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

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

    end;

    theorem :: MATRIXR2:8

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

    proof

      let A,B be Matrix of REAL ;

      assume that

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

       A2: ( len A) > 0 ;

      

      thus ((A + B) - B) = ((A + B) + ( - B)) by MATRIX_4:def 1

      .= (A + (B + ( - B))) by A1, MATRIX_3: 3

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

      .= A by A1, A2, Th7;

    end;

    

     Lm3: for A be Matrix of REAL st [i, j] in ( Indices A) holds (( - A) * (i,j)) = ( - (A * (i,j)))

    proof

      let A be Matrix of REAL ;

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

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

      hence thesis;

    end;

    theorem :: MATRIXR2:9

    

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

    proof

      let A be Matrix of REAL ;

      

       A1: ( width (( - 1) * A)) = ( width A) by Th5;

      

       A2: ( len (( - 1) qua Real * A)) = ( len A) by Th5;

       A3:

      now

        let i,j be Nat;

        reconsider i0 = i, j0 = j as Nat;

        assume

         A4: [i, j] in ( Indices (( - 1) * A));

        then

         A5: 1 <= j0 & j0 <= ( width A) by A1, MATRIXC1: 1;

        1 <= i0 & i0 <= ( len A) by A2, A4, MATRIXC1: 1;

        then

         A6: [i0, j0] in ( Indices A) by A5, MATRIXC1: 1;

        

        hence ((( - 1) * A) * (i,j)) = (( - 1) * (A * (i0,j0))) by Th3

        .= ( - (A * (i,j)))

        .= (( - A) * (i,j)) by A6, Lm3;

      end;

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

      hence thesis by A2, A1, A3, MATRIX_0: 21;

    end;

    theorem :: MATRIXR2:10

    

     Th10: for A be Matrix of REAL , i,j be Nat st [i, j] in ( Indices A) holds (( - A) * (i,j)) = ( - (A * (i,j)))

    proof

      let A be Matrix of REAL , i,j be Nat;

      assume

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

      ( - A) = (( - 1) * A) by Th9;

      then (( - A) * (i,j)) = (( - 1) * (A * (i,j))) by A1, MATRIXR1: 29;

      hence thesis;

    end;

    theorem :: MATRIXR2:11

    for a,b be Real, A be Matrix of REAL holds ((a * b) * A) = (a * (b * A))

    proof

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

      

       A1: ( len ((a * b) * A)) = ( len A) & ( width ((a * b) * A)) = ( width A) by Th5;

      

       A2: ( len (a * (b * A))) = ( len (b * A)) by Th5;

      

       A3: ( width (a * (b * A))) = ( width (b * A)) by Th5;

      then

       A4: ( width (a * (b * A))) = ( width A) by Th5;

      

       A5: ( len (b * A)) = ( len A) & ( width (b * A)) = ( width A) by Th5;

      

       A6: for i,j be Nat st [i, j] in ( Indices (a * (b * A))) holds ((a * (b * A)) * (i,j)) = (((a * b) * A) * (i,j))

      proof

        let i,j be Nat;

        assume

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

        

         A8: ( Indices (b * A)) = ( Indices A) by A5, MATRIX_4: 55;

        reconsider i0 = i, j0 = j as Nat;

        

         A9: ( Indices (a * (b * A))) = ( Indices (b * A)) by A2, A3, MATRIX_4: 55;

        

        then ((a * (b * A)) * (i,j)) = (a * ((b * A) * (i0,j0))) by A7, Th3

        .= (a * (b * (A * (i0,j0)))) by A7, A9, A8, Th3

        .= ((a * b) * (A * (i0,j0)))

        .= (((a * b) * A) * (i,j)) by A7, A9, A8, Th3;

        hence thesis;

      end;

      ( len (a * (b * A))) = ( len A) by A2, Th5;

      hence thesis by A1, A4, A6, MATRIX_0: 21;

    end;

    theorem :: MATRIXR2:12

    

     Th12: for a,b be Real, A be Matrix of REAL holds ((a + b) * A) = ((a * A) + (b * A))

    proof

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

      

       A1: ( len (a * A)) = ( len A) & ( width (a * A)) = ( width A) by MATRIXR1: 27;

      

       A2: ( len ((a + b) * A)) = ( len A) & ( width ((a + b) * A)) = ( width A) by MATRIXR1: 27;

      

       A3: for i,j be Nat st [i, j] in ( Indices ((a + b) * A)) holds (((a + b) * A) * (i,j)) = (((a * A) + (b * A)) * (i,j))

      proof

        let i,j be Nat;

        assume

         A4: [i, j] in ( Indices ((a + b) * A));

        reconsider i0 = i, j0 = j as Nat;

        

         A5: ( Indices ((a + b) * A)) = ( Indices A) by A2, MATRIX_4: 55;

        ( Indices (a * A)) = ( Indices A) by A1, MATRIX_4: 55;

        

        then (((a * A) + (b * A)) * (i,j)) = (((a * A) * (i0,j0)) + ((b * A) * (i0,j0))) by A4, A5, MATRIXR1: 25

        .= ((a * (A * (i0,j0))) + ((b * A) * (i0,j0))) by A4, A5, MATRIXR1: 29

        .= ((a * (A * (i0,j0))) + (b * (A * (i0,j0)))) by A4, A5, MATRIXR1: 29

        .= ((a + b) * (A * (i,j)));

        hence thesis by A4, A5, MATRIXR1: 29;

      end;

      ( len ((a * A) + (b * A))) = ( len (a * A)) & ( width ((a * A) + (b * A))) = ( width (a * A)) by MATRIX_3:def 3;

      hence thesis by A2, A1, A3, MATRIX_0: 21;

    end;

    theorem :: MATRIXR2:13

    for a,b be Real, A be Matrix of REAL holds ((a - b) * A) = ((a * A) - (b * A))

    proof

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

      

       A1: ( len ((a - b) * A)) = ( len A) & ( width ((a - b) * A)) = ( width A) by MATRIXR1: 27;

      

       A2: ( len (a * A)) = ( len A) & ( width (a * A)) = ( width A) by MATRIXR1: 27;

      

       A3: ( len (b * A)) = ( len A) & ( width (b * A)) = ( width A) by MATRIXR1: 27;

      

       A4: for i,j be Nat st [i, j] in ( Indices ((a - b) * A)) holds (((a - b) * A) * (i,j)) = (((a * A) - (b * A)) * (i,j))

      proof

        let i,j be Nat;

        assume

         A5: [i, j] in ( Indices ((a - b) * A));

        reconsider i0 = i, j0 = j as Nat;

        

         A6: ( Indices ((a - b) * A)) = ( Indices A) by A1, MATRIX_4: 55;

        ( Indices (a * A)) = ( Indices A) by A2, MATRIX_4: 55;

        

        then (((a * A) - (b * A)) * (i,j)) = (((a * A) * (i0,j0)) - ((b * A) * (i0,j0))) by A2, A3, A5, A6, Th6

        .= ((a * (A * (i0,j0))) - ((b * A) * (i0,j0))) by A5, A6, MATRIXR1: 29

        .= ((a * (A * (i0,j0))) - (b * (A * (i0,j0)))) by A5, A6, MATRIXR1: 29

        .= ((a - b) * (A * (i,j)));

        hence thesis by A5, A6, MATRIXR1: 29;

      end;

      

       A7: ( width ((a * A) - (b * A))) = ( width ( MXF2MXR (( MXR2MXF (a * A)) + ( - ( MXR2MXF (b * A)))))) by MATRIX_4:def 1

      .= ( width (a * A)) by MATRIX_3:def 3;

      ( len ((a * A) - (b * A))) = ( len ( MXF2MXR (( MXR2MXF (a * A)) + ( - ( MXR2MXF (b * A)))))) by MATRIX_4:def 1

      .= ( len (a * A)) by MATRIX_3:def 3;

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

    end;

    theorem :: MATRIXR2:14

    

     Th14: for A be Matrix of K st n > 0 & ( len A) > 0 holds (( 0. (K,n,( len A))) * A) = ( 0. (K,n,( width A)))

    proof

      let A be Matrix of K;

      assume that

       A1: n > 0 and

       A2: ( len A) > 0 ;

      

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

      then

       A4: ( width ( 0. (K,n,( len A)))) = ( len A) by A1, MATRIX_0: 20;

      then

       A5: ( len (( 0. (K,n,( len A))) * A)) = n by A3, MATRIX_3:def 4;

      

       A6: ( width (( 0. (K,n,( len A))) * A)) = ( width A) by A4, MATRIX_3:def 4;

      ((( 0. (K,n,( len A))) * A) + (( 0. (K,n,( len A))) * A)) = ((( 0. (K,n,( len A))) + ( 0. (K,n,( len A)))) * A) by A1, A2, A3, A4, MATRIX_4: 63

      .= (( 0. (K,n,( len A))) * A) by MATRIX_3: 4;

      hence thesis by A5, A6, MATRIX_4: 6;

    end;

    theorem :: MATRIXR2:15

    

     Th15: for A,C be Matrix of K st ( len A) = ( width C) & ( len C) > 0 & ( len A) > 0 holds (( - C) * A) = ( - (C * A))

    proof

      let A,C be Matrix of K;

      assume that

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

       A2: ( len C) > 0 and

       A3: ( len A) > 0 ;

      

       A4: ( len C) = ( len ( - C)) by MATRIX_3:def 2;

      

       A5: ( width ( - C)) = ( width C) by MATRIX_3:def 2;

      then ( width (( - C) * A)) = ( width A) by A1, MATRIX_3:def 4;

      then

       A6: ( width (C * A)) = ( width (( - C) * A)) by A1, MATRIX_3:def 4;

      reconsider D = C as Matrix of ( len C), ( width C), K by A2, MATRIX_0: 20;

      

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

      then

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

      ( len ( - C)) = ( len (( - C) * A)) by A1, A5, MATRIX_3:def 4;

      then

       A9: ( len (C * A)) = ( len (( - C) * A)) by A1, A4, MATRIX_3:def 4;

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

      

      then ((C * A) + (( - C) * A)) = ((D + ( - D)) * A) by A1, A2, A3, A7, MATRIX_4: 63

      .= (( 0. (K,( len C),( width C))) * A) by MATRIX_3: 5

      .= ( 0. (K,( len C),( width A))) by A1, A2, A3, Th14;

      hence thesis by A4, A8, A9, A6, MATRIX_4: 8;

    end;

    theorem :: MATRIXR2:16

    

     Th16: for 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 A,B,C be Matrix of K;

      assume

       A1: ( len B) = ( len C) & ( width B) = ( width C) & ( len A) = ( width B) & ( len B) > 0 & ( len A) > 0 ;

      

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

      

      thus ((B - C) * A) = ((B + ( - C)) * A) by MATRIX_4:def 1

      .= ((B * A) + (( - C) * A)) by A1, A2, MATRIX_4: 63

      .= ((B * A) + ( - (C * A))) by A1, Th15

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

    end;

    theorem :: MATRIXR2:17

    for A,B,C be Matrix of REAL st ( len A) = ( len B) & ( width A) = ( width B) & ( len C) = ( width A) & ( len A) > 0 & ( len C) > 0 holds ((A - B) * C) = ((A * C) - (B * C)) by Th16;

    theorem :: MATRIXR2:18

    

     Th18: for m be Nat, A,C be Matrix of K st ( width A) > 0 & ( len A) > 0 holds (A * ( 0. (K,( width A),m))) = ( 0. (K,( len A),m))

    proof

      let m be Nat, A,C be Matrix of K;

      assume that

       A1: ( width A) > 0 and

       A2: ( len A) > 0 ;

      

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

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

      then

       A4: ( width (A * ( 0. (K,( width A),m)))) = m by A3, MATRIX_3:def 4;

      ( width ( 0. (K,( width A),m))) = m by A1, A3, MATRIX_0: 20;

      

      then

       A5: ((A * ( 0. (K,( width A),m))) + (A * ( 0. (K,( width A),m)))) = (A * (( 0. (K,( width A),m)) + ( 0. (K,( width A),m)))) by A1, A2, A3, MATRIX_4: 62

      .= (A * ( 0. (K,( width A),m))) by MATRIX_3: 4;

      ( len (A * ( 0. (K,( width A),m)))) = ( len A) by A3, MATRIX_3:def 4;

      hence thesis by A4, A5, MATRIX_4: 6;

    end;

    theorem :: MATRIXR2:19

    

     Th19: for A,C be Matrix of K st ( width A) = ( len C) & ( len A) > 0 & ( len C) > 0 holds (A * ( - C)) = ( - (A * C))

    proof

      let A,C be Matrix of K;

      assume that

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

       A2: ( len A) > 0 and

       A3: ( len C) > 0 ;

      

       A4: ( len C) = ( len ( - C)) by MATRIX_3:def 2;

      then

       A5: ( len A) = ( len (A * ( - C))) by A1, MATRIX_3:def 4;

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

      then

       A6: ( width (A * ( - C))) = ( width C) by A1, A4, MATRIX_3:def 4;

      reconsider D = C as Matrix of ( len C), ( width C), K by A3, MATRIX_0: 20;

      

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

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

      

      then ((A * C) + (A * ( - C))) = (A * (D + ( - D))) by A1, A2, A3, MATRIX_4: 62

      .= (A * ( 0. (K,( len C),( width C)))) by MATRIX_3: 5

      .= ( 0. (K,( len A),( width C))) by A1, A2, A3, Th18;

      hence thesis by A7, A5, A6, MATRIX_4: 8;

    end;

    theorem :: MATRIXR2:20

    

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

    proof

      let A,B,C be Matrix of K;

      assume that

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

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

       A3: ( len B) = ( width A) & ( len B) > 0 & ( len A) > 0 ;

      

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

      

      thus (A * (B - C)) = (A * (B + ( - C))) by MATRIX_4:def 1

      .= ((A * B) + (A * ( - C))) by A1, A2, A3, A4, MATRIX_4: 62

      .= ((A * B) + ( - (A * C))) by A1, A3, Th19

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

    end;

    theorem :: MATRIXR2:21

    for A,B,C be Matrix of REAL st ( len A) = ( len B) & ( width A) = ( width B) & ( width C) = ( len A) & ( len C) > 0 & ( len A) > 0 holds (C * (A - B)) = ((C * A) - (C * B)) by Th20;

    theorem :: MATRIXR2:22

    

     Th22: for A,B,C be Matrix of REAL st ( len A) = ( len B) & ( width A) = ( width B) & ( len C) = ( len A) & ( width C) = ( width A) & (for i,j be Nat 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 A) = ( len B) & ( width A) = ( width B) and

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

       A3: for i,j be Nat st [i, j] in ( Indices A) holds (C * (i,j)) = ((A * (i,j)) - (B * (i,j)));

      

       A4: ( Indices B) = ( Indices A) by A1, MATRIX_4: 55;

      for i,j be Nat st [i, j] in ( Indices A) holds (C * (i,j)) = ((A * (i,j)) + (( - B) * (i,j)))

      proof

        let i,j be Nat;

        reconsider i0 = i, j0 = j as Nat;

        assume

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

        

        hence (C * (i,j)) = ((A * (i0,j0)) - (B * (i0,j0))) by A3

        .= ((A * (i0,j0)) + ( - (B * (i0,j0))))

        .= ((A * (i,j)) + (( - B) * (i,j))) by A4, A5, Th10;

      end;

      then C = (A + ( - B)) by A2, MATRIXR1: 26;

      hence thesis by MATRIX_4:def 1;

    end;

    theorem :: MATRIXR2:23

    

     Th23: 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 ;

      

       A1: ( width ( LineVec2Mx x1)) = ( len x1) & ( len ( LineVec2Mx x1)) = 1 by MATRIXR1:def 10;

      

       A2: ( Seg ( width ( LineVec2Mx x1))) = ( Seg ( len x1)) by MATRIXR1:def 10

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

      

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

      .= ( Seg 1) by MATRIXR1:def 10;

      assume

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

      then

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

      

       A6: ( width ( LineVec2Mx x2)) = ( len x2) & ( len ( LineVec2Mx x2)) = 1 by MATRIXR1:def 10;

      then

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

      

       A8: ( len (x1 - x2)) = ( len x1) by A4, RVSUM_1: 116;

      then

       A9: ( dom (x1 - x2)) = ( dom x1) by FINSEQ_3: 29;

      

       A10: ( width ( LineVec2Mx (x1 - x2))) = ( len (x1 - x2)) & ( len ( LineVec2Mx (x1 - x2))) = 1 by MATRIXR1:def 10;

      then

       A11: ( Indices ( LineVec2Mx (x1 - x2))) = ( Indices ( LineVec2Mx x1)) by A4, A1, MATRIX_4: 55, RVSUM_1: 116;

      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

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

        then

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

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

        i in ( Seg 1) by A3, A12, ZFMISC_1: 87;

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

        then

         A14: i = 1 by XXREAL_0: 1;

        

         A15: j in ( dom x1) by A2, A12, ZFMISC_1: 87;

        then

         A16: (q1 . j) = (x1 . j) by A14, A13, MATRIXR1:def 10;

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

         A17: (( LineVec2Mx (x1 - x2)) * (i,j)) = (p . j) by A11, A12, MATRIX_0:def 5;

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

         A18: (( LineVec2Mx x2) * (i,j)) = (q2 . j) by A7, A12, MATRIX_0:def 5;

        

         A19: (q2 . j) = (x2 . j) by A5, A15, A14, A18, MATRIXR1:def 10;

        (p . j) = ((x1 - x2) . j) by A9, A15, A14, A17, MATRIXR1:def 10;

        hence thesis by A4, A17, A13, A16, A18, A19, Lm1;

      end;

      hence thesis by A4, A8, A10, A1, A6, Th22;

    end;

    theorem :: MATRIXR2:24

    

     Th24: 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, MATRIXR1:def 9;

      

       A4: ( Seg ( width ( ColVec2Mx x1))) = ( Seg 1) by A2, MATRIXR1:def 9;

      

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

      

       A6: ( len (x1 - x2)) = ( len x1) by A1, RVSUM_1: 116;

      then

       A7: ( dom (x1 - x2)) = ( dom x1) by FINSEQ_3: 29;

      

       A8: ( len ( ColVec2Mx x1)) = ( len x1) by A2, MATRIXR1:def 9;

      then

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

      

       A10: ( len ( ColVec2Mx x2)) = ( len x2) & ( width ( ColVec2Mx x2)) = 1 by A1, A2, MATRIXR1:def 9;

      then

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

      

       A12: ( len ( ColVec2Mx (x1 - x2))) = ( len (x1 - x2)) & ( width ( ColVec2Mx (x1 - x2))) = 1 by A2, A6, MATRIXR1:def 9;

      then

       A13: ( Indices ( ColVec2Mx (x1 - x2))) = ( Indices ( ColVec2Mx x1)) by A1, A8, A3, MATRIX_4: 55, RVSUM_1: 116;

      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;

        assume

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

        then

        consider q1 be FinSequence of REAL such that

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

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

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

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

        then

         A17: j = 1 by XXREAL_0: 1;

        

         A18: i in ( dom x1) by A9, A14, ZFMISC_1: 87;

        then (( ColVec2Mx x1) . i) = <*(x1 . i)*> by A2, MATRIXR1:def 9;

        then

         A19: (q1 . j) = (x1 . i) by A17, A15, FINSEQ_1: 40;

        consider p be FinSequence of REAL such that

         A20: p = (( ColVec2Mx (x1 - x2)) . i) and

         A21: (( ColVec2Mx (x1 - x2)) * (i,j)) = (p . j) by A13, A14, MATRIX_0:def 5;

        consider q2 be FinSequence of REAL such that

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

         A23: (( ColVec2Mx x2) * (i,j)) = (q2 . j) by A11, A14, MATRIX_0:def 5;

        (( ColVec2Mx x2) . i) = <*(x2 . i)*> by A1, A2, A5, A18, MATRIXR1:def 9;

        then

         A24: (q2 . j) = (x2 . i) by A17, A22, FINSEQ_1: 40;

        (( ColVec2Mx (x1 - x2)) . i) = <*((x1 - x2) . i)*> by A2, A6, A7, A18, MATRIXR1:def 9;

        then (p . j) = ((x1 - x2) . i) by A17, A20, FINSEQ_1: 40;

        hence thesis by A1, A21, A16, A19, A23, A24, Lm1;

      end;

      hence thesis by A1, A6, A8, A12, A3, A10, Th22;

    end;

    theorem :: MATRIXR2:25

    

     Th25: for A,B be Matrix of REAL st ( len A) = ( len B) & ( 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 that

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

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

      

       A3: ( width (A - B)) = ( width A) by A1, A2, Th6;

      let i be Nat;

      

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

      

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

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

      then

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

      

       A7: for j be Nat st j in ( Seg ( width (A - B))) holds ((( Line (A,i)) - ( Line (B,i))) . j) = ((A - B) * (i,j))

      proof

        reconsider i2 = i as Nat;

        let j be Nat;

        reconsider j2 = j as Nat;

        

         A8: ((( Line (A,i2)) - ( Line (B,i2))) . j) = ((( Line (A,i2)) . j2) - (( Line (B,i2)) . j2)) by A2, A4, A5, Lm1;

        assume

         A9: j in ( Seg ( width (A - B)));

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

        then

         A10: ((A - B) * (i2,j2)) = ((A * (i2,j2)) - (B * (i2,j2))) by A1, A2, Th6;

        

         A11: j in ( Seg ( width A)) by A1, A2, A9, Th6;

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

        hence thesis by A2, A11, A10, A8, MATRIX_0:def 7;

      end;

      ( len (( Line (A,i)) - ( Line (B,i)))) = ( len ( Line (A,i))) by A2, A4, A5, RVSUM_1: 116;

      hence thesis by A4, A3, A7, MATRIX_0:def 7;

    end;

    theorem :: MATRIXR2:26

    

     Th26: for A,B be Matrix of REAL st ( len A) = ( len B) & ( width A) = ( width 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 that

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

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

      

       A3: ( len (A - B)) = ( len A) by A1, A2, Th6;

      let i be Nat;

      

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

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

      then

       A5: i in ( Seg ( width A));

      

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

      

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

      

       A8: for j be Nat st j in ( dom (A - B)) holds ((( Col (A,i)) - ( Col (B,i))) . j) = ((A - B) * (j,i))

      proof

        let j be Nat;

        assume j in ( dom (A - B));

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

        then

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

        then

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

        reconsider j as Nat;

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

        then ((( Col (A,i)) . j) - (( Col (B,i)) . j)) = ((A - B) * (j,i)) by A1, A2, A10, Th6;

        hence thesis by A1, A4, A6, Lm1;

      end;

      ( len (( Col (A,i)) - ( Col (B,i)))) = ( len ( Col (A,i))) by A1, A4, A6, RVSUM_1: 116;

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

    end;

    theorem :: MATRIXR2:27

    for A be Matrix of n, k, REAL , B be Matrix of k, m, REAL , C be Matrix of m, l, REAL st n > 0 & k > 0 & m > 0 holds ((A * B) * C) = (A * (B * C))

    proof

      let A be Matrix of n, k, REAL , B be Matrix of k, m, REAL , C be Matrix of m, l, REAL ;

      assume that

       A1: n > 0 and

       A2: k > 0 and

       A3: m > 0 ;

      

       A4: ( width B) = m & ( len C) = m by A2, A3, MATRIX_0: 23;

      ( width A) = k & ( len B) = k by A1, A2, MATRIX_0: 23;

      hence thesis by A4, MATRIX_3: 33;

    end;

    theorem :: MATRIXR2:28

    

     Th28: for A,B,C be Matrix of n, REAL holds ((A * B) * C) = (A * (B * C))

    proof

      let A,B,C be Matrix of n, REAL ;

      

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

      ( width A) = n & ( len B) = n by MATRIX_0: 24;

      hence thesis by A1, MATRIX_3: 33;

    end;

    theorem :: MATRIXR2:29

    

     Th29: for A be Matrix of n, D holds ((A @ ) @ ) = A

    proof

      let A be Matrix of n, D;

      reconsider N = (A @ ) as Matrix of n, D;

      

       A1: ( len A) = n & ( width A) = n by MATRIX_0: 24;

      

       A2: ( Indices (N @ )) = [:( Seg n), ( Seg n):] by MATRIX_0: 24

      .= ( Indices A) by MATRIX_0: 24;

      

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

      proof

        let i,j be Nat;

        assume

         A4: [i, j] in ( Indices (N @ ));

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

        then ((N @ ) * (i,j)) = (N * (j,i)) by MATRIX_0:def 6;

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

      end;

      ( len (N @ )) = n & ( width (N @ )) = n by MATRIX_0: 24;

      hence thesis by A1, A3, MATRIX_0: 21;

    end;

    theorem :: MATRIXR2:30

    

     Th30: for A,B be Matrix of n, REAL holds ((A * B) @ ) = ((B @ ) * (A @ ))

    proof

      let A,B be Matrix of n, REAL ;

      

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

      

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

      

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

      

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

      

       A5: ( len (B @ )) = n by MATRIX_0: 24;

      then

       A6: ( len ((B @ ) * (A @ ))) = ( len (B @ )) by MATRIX_0: 24;

      

       A7: ( width (B @ )) = n by MATRIX_0: 24

      .= ( len (A @ )) by MATRIX_0: 24;

      

       A8: ( width (A * B)) = n by MATRIX_0: 24;

      

       A9: ( width (A @ )) = n by MATRIX_0: 24;

      then

       A10: ( width ((B @ ) * (A @ ))) = ( width (A @ )) by MATRIX_0: 24;

       A11:

      now

        let i,j be Nat;

        

         A12: ( Indices ((A * B) @ )) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        assume

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

        then j in ( Seg ( len (A * B))) by A3, A12, ZFMISC_1: 87;

        then

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

        i in ( Seg ( width (A * B))) by A8, A13, A12, ZFMISC_1: 87;

        then

         A15: [j, i] in ( Indices (A * B)) by A14, ZFMISC_1: 87;

        ( Seg ( width (A @ ))) = ( dom A) by A1, A9, FINSEQ_1:def 3;

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

        then

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

        reconsider i0 = i, j0 = j as Nat;

        

         A17: ( Seg ( width B)) = ( dom (B @ )) by A4, A5, FINSEQ_1:def 3;

        

         A18: ( Indices ((B @ ) * (A @ ))) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        then [i, j] in [:( dom (B @ )), ( Seg ( width (A @ ))):] by A6, A10, A13, A12, FINSEQ_3: 29;

        then i in ( Seg ( width B)) by A17, ZFMISC_1: 87;

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

        

        hence (((B @ ) * (A @ )) * (i,j)) = (( Col (B,i0)) "*" ( Line (A,j0))) by A7, A13, A12, A18, A16, MATRPROB: 39

        .= ((A * B) * (j0,i0)) by A2, A15, MATRPROB: 39

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

      end;

      

       A19: ( len ((B @ ) * (A @ ))) = n & ( width ((B @ ) * (A @ ))) = n by MATRIX_0: 24;

      ( len ((A * B) @ )) = n & ( width ((A * B) @ )) = n by MATRIX_0: 24;

      hence thesis by A19, A11, MATRIX_0: 21;

    end;

    theorem :: MATRIXR2:31

    

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

    proof

      let A be Matrix of REAL ;

      assume

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

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

      

      hence (( - A) + A) = ( MXF2MXR (( MXR2MXF A) + ( - ( MXR2MXF A)))) by MATRIX_3: 2

      .= ( 0_Rmatrix (n,m)) by A1, MATRIX_4: 2;

    end;

    begin

    definition

      let n;

      let A be Matrix of n, REAL ;

      :: original: MXR2MXF

      redefine

      func MXR2MXF A -> Matrix of n, F_Real ;

      coherence ;

    end

    definition

      let n;

      let A be Matrix of n, REAL ;

      :: MATRIXR2:def1

      func Det A -> Real equals ( Det ( MXR2MXF A));

      coherence ;

    end

    theorem :: MATRIXR2:32

    for A be Matrix of 2, REAL holds ( Det A) = (((A * (1,1)) * (A * (2,2))) - ((A * (1,2)) * (A * (2,1))))

    proof

      let A be Matrix of 2, REAL ;

      reconsider N = ( MXR2MXF A) as Matrix of 2, F_Real ;

      ( Det A) = (((N * (1,1)) * (N * (2,2))) - ((N * (1,2)) * (N * (2,1)))) by MATRIX_7: 12;

      hence thesis;

    end;

    theorem :: MATRIXR2:33

    

     Th33: for s1,s2,s3 be FinSequence st ( len s1) = n & ( len s2) = n & ( len s3) = n holds <*s1, s2, s3*> is tabular

    proof

      let s1,s2,s3 be FinSequence;

      assume

       A1: ( len s1) = n & ( len s2) = n & ( len s3) = n;

      now

        take n;

        let x be object;

        assume x in ( rng <*s1, s2, s3*>);

        then

         A2: x in {s1, s2, s3} by FINSEQ_2: 128;

        then

        reconsider r = x as FinSequence by ENUMSET1:def 1;

        take r;

        thus x = r & ( len r) = n by A1, A2, ENUMSET1:def 1;

      end;

      hence thesis;

    end;

    theorem :: MATRIXR2:34

    

     Th34: for p1,p2,p3 be FinSequence of D st ( len p1) = n & ( len p2) = n & ( len p3) = n holds <*p1, p2, p3*> is Matrix of 3, n, D

    proof

      let p1,p2,p3 be FinSequence of D;

      reconsider q1 = p1, q2 = p2, q3 = p3 as Element of (D * ) by FINSEQ_1:def 11;

      reconsider M = <*q1, q2, q3*> as FinSequence of (D * );

      assume

       A1: ( len p1) = n & ( len p2) = n & ( len p3) = n;

      then

      reconsider M as Matrix of D by Th33;

      M is 3, n -size

      proof

        thus ( len M) = 3 by FINSEQ_1: 45;

        let r be FinSequence of D;

        assume r in ( rng M);

        then r in {p1, p2, p3} by FINSEQ_2: 128;

        hence thesis by A1, ENUMSET1:def 1;

      end;

      hence thesis;

    end;

    theorem :: MATRIXR2:35

    

     Th35: for a1,a2,a3,b1,b2,b3,c1,c2,c3 be Element of D holds <* <*a1, a2, a3*>, <*b1, b2, b3*>, <*c1, c2, c3*>*> is Matrix of 3, D

    proof

      let a1,a2,a3,b1,b2,b3,c1,c2,c3 be Element of D;

      

       A1: ( len <*c1, c2, c3*>) = 3 by FINSEQ_1: 45;

      ( len <*a1, a2, a3*>) = 3 & ( len <*b1, b2, b3*>) = 3 by FINSEQ_1: 45;

      hence thesis by A1, Th34;

    end;

    theorem :: MATRIXR2:36

    

     Th36: for A be Matrix of n, D holds for p be FinSequence of D, i be Nat st p = (A . i) & i in ( Seg n) holds ( len p) = n

    proof

      let A be Matrix of n, D;

      let p be FinSequence of D, i be Nat;

      assume that

       A1: p = (A . i) and

       A2: i in ( Seg n);

      consider n2 be Nat such that

       A3: for x be object st x in ( rng A) holds ex s be FinSequence of D st s = x & ( len s) = n2 by MATRIX_0: 9;

      ( len A) = n by MATRIX_0: 24;

      then

       A4: i in ( dom A) by A2, FINSEQ_1:def 3;

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

      then

      consider s be FinSequence of D such that

       A5: s = (A . i) and ( len s) = n2 by A3;

      s in ( rng A) by A4, A5, FUNCT_1:def 3;

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

    end;

    theorem :: MATRIXR2:37

    

     Th37: for A be Matrix of 3, D holds A = <* <*(A * (1,1)), (A * (1,2)), (A * (1,3))*>, <*(A * (2,1)), (A * (2,2)), (A * (2,3))*>, <*(A * (3,1)), (A * (3,2)), (A * (3,3))*>*>

    proof

      let A be Matrix of 3, D;

      reconsider B = <* <*(A * (1,1)), (A * (1,2)), (A * (1,3))*>, <*(A * (2,1)), (A * (2,2)), (A * (2,3))*>, <*(A * (3,1)), (A * (3,2)), (A * (3,3))*>*> as Matrix of 3, D by Th35;

      

       A1: ( len A) = 3 & ( width A) = 3 by MATRIX_0: 24;

      

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

      proof

        let i,j be Nat;

        

         A3: ( Indices B) = [:( Seg 3), ( Seg 3):] by MATRIX_0: 24;

        

         A4: ( Indices A) = [:( Seg 3), ( Seg 3):] by MATRIX_0: 24;

        assume

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

        then

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

        2 in ( Seg 3);

        then

         A7: [i, 2] in ( Indices A) by A4, A6, ZFMISC_1: 87;

        1 in ( Seg 3);

        then

         A8: [i, 1] in ( Indices A) by A4, A6, ZFMISC_1: 87;

        3 in ( Seg 3);

        then

         A9: [i, 3] in ( Indices A) by A4, A6, ZFMISC_1: 87;

        

         A10: i in {1, 2, 3} by A5, A4, FINSEQ_3: 1, ZFMISC_1: 87;

        now

          per cases by A10, ENUMSET1:def 1;

            case

             A11: i = 1;

            reconsider p0 = <*(A * (1,1)), (A * (1,2)), (A * (1,3))*> as FinSequence of D;

            

             A12: ( len p0) = 3 by FINSEQ_1: 45;

            

             A13: ex p23 be FinSequence of D st p23 = (A . i) & (A * (i,3)) = (p23 . 3) by A9, MATRIX_0:def 5;

            consider p2 be FinSequence of D such that

             A14: p2 = (A . i) and

             A15: (A * (i,1)) = (p2 . 1) by A8, MATRIX_0:def 5;

            

             A16: ex p22 be FinSequence of D st p22 = (A . i) & (A * (i,2)) = (p22 . 2) by A7, MATRIX_0:def 5;

            

             A17: for k be Nat st 1 <= k & k <= ( len p0) holds (p0 . k) = (p2 . k)

            proof

              let k be Nat;

              assume

               A18: 1 <= k & k <= ( len p0);

              

               A19: k in ( Seg 3) by A12, A18;

              per cases by A19, ENUMSET1:def 1, FINSEQ_3: 1;

                suppose k = 1;

                hence thesis by A11, A15, FINSEQ_1: 45;

              end;

                suppose k = 2;

                hence thesis by A11, A14, A16, FINSEQ_1: 45;

              end;

                suppose k = 3;

                hence thesis by A11, A14, A13, FINSEQ_1: 45;

              end;

            end;

            ex p be FinSequence of D st p = (B . i) & (B * (i,j)) = (p . j) by A5, A3, A4, MATRIX_0:def 5;

            then

             A20: (B * (i,j)) = (p0 . j) by A11, FINSEQ_1: 45;

            ( len p2) = 3 by A6, A14, Th36;

            hence ex p be FinSequence of D st p = (A . i) & (B * (i,j)) = (p . j) by A12, A14, A17, A20, FINSEQ_1: 14;

          end;

            case

             A21: i = 2;

            reconsider p0 = <*(A * (2,1)), (A * (2,2)), (A * (2,3))*> as FinSequence of D;

            

             A22: ( len p0) = 3 by FINSEQ_1: 45;

            

             A23: ex p23 be FinSequence of D st p23 = (A . i) & (A * (i,3)) = (p23 . 3) by A9, MATRIX_0:def 5;

            consider p2 be FinSequence of D such that

             A24: p2 = (A . i) and

             A25: (A * (i,1)) = (p2 . 1) by A8, MATRIX_0:def 5;

            

             A26: ex p22 be FinSequence of D st p22 = (A . i) & (A * (i,2)) = (p22 . 2) by A7, MATRIX_0:def 5;

            

             A27: for k be Nat st 1 <= k & k <= ( len p0) holds (p0 . k) = (p2 . k)

            proof

              let k be Nat;

              assume

               A28: 1 <= k & k <= ( len p0);

              

               A29: k in {1, 2, 3} by A22, A28, FINSEQ_3: 1;

              per cases by A29, ENUMSET1:def 1;

                suppose k = 1;

                hence thesis by A21, A25, FINSEQ_1: 45;

              end;

                suppose k = 2;

                hence thesis by A21, A24, A26, FINSEQ_1: 45;

              end;

                suppose k = 3;

                hence thesis by A21, A24, A23, FINSEQ_1: 45;

              end;

            end;

            ex p be FinSequence of D st p = (B . i) & (B * (i,j)) = (p . j) by A5, A3, A4, MATRIX_0:def 5;

            then

             A30: (B * (i,j)) = (p0 . j) by A21, FINSEQ_1: 45;

            ( len p2) = 3 by A6, A24, Th36;

            hence ex p be FinSequence of D st p = (A . i) & (B * (i,j)) = (p . j) by A22, A24, A27, A30, FINSEQ_1: 14;

          end;

            case

             A31: i = 3;

            reconsider p0 = <*(A * (3,1)), (A * (3,2)), (A * (3,3))*> as FinSequence of D;

            

             A32: ( len p0) = 3 by FINSEQ_1: 45;

            

             A33: ex p23 be FinSequence of D st p23 = (A . i) & (A * (i,3)) = (p23 . 3) by A9, MATRIX_0:def 5;

            consider p2 be FinSequence of D such that

             A34: p2 = (A . i) and

             A35: (A * (i,1)) = (p2 . 1) by A8, MATRIX_0:def 5;

            

             A36: ex p22 be FinSequence of D st p22 = (A . i) & (A * (i,2)) = (p22 . 2) by A7, MATRIX_0:def 5;

            

             A37: for k be Nat st 1 <= k & k <= ( len p0) holds (p0 . k) = (p2 . k)

            proof

              let k be Nat;

              assume

               A38: 1 <= k & k <= ( len p0);

              

               A39: k in {1, 2, 3} by A32, A38, FINSEQ_3: 1;

              per cases by A39, ENUMSET1:def 1;

                suppose k = 1;

                hence thesis by A31, A35, FINSEQ_1: 45;

              end;

                suppose k = 2;

                hence thesis by A31, A34, A36, FINSEQ_1: 45;

              end;

                suppose k = 3;

                hence thesis by A31, A34, A33, FINSEQ_1: 45;

              end;

            end;

            ex p be FinSequence of D st p = (B . i) & (B * (i,j)) = (p . j) by A5, A3, A4, MATRIX_0:def 5;

            then

             A40: (B * (i,j)) = (p0 . j) by A31, FINSEQ_1: 45;

            ( len p2) = 3 by A6, A34, Th36;

            hence ex p be FinSequence of D st p = (A . i) & (B * (i,j)) = (p . j) by A32, A34, A37, A40, FINSEQ_1: 14;

          end;

        end;

        hence thesis by A5, MATRIX_0:def 5;

      end;

      ( len B) = 3 & ( width B) = 3 by MATRIX_0: 24;

      hence thesis by A1, A2, MATRIX_0: 21;

    end;

    theorem :: MATRIXR2:38

    for A be Matrix of 3, REAL holds ( Det A) = ((((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2))))

    proof

      let A be Matrix of 3, REAL ;

      reconsider N = ( MXR2MXF A) as Matrix of 3, F_Real ;

      reconsider N2 = <* <*(N * (1,1)), (N * (1,2)), (N * (1,3))*>, <*(N * (2,1)), (N * (2,2)), (N * (2,3))*>, <*(N * (3,1)), (N * (3,2)), (N * (3,3))*>*> as Matrix of 3, F_Real by Th35;

      ( Det A) = ( Det N2) by Th37

      .= ((((((((N * (1,1)) * (N * (2,2))) * (N * (3,3))) - (((N * (1,3)) * (N * (2,2))) * (N * (3,1)))) - (((N * (1,1)) * (N * (2,3))) * (N * (3,2)))) + (((N * (1,2)) * (N * (2,3))) * (N * (3,1)))) - (((N * (1,2)) * (N * (2,1))) * (N * (3,3)))) + (((N * (1,3)) * (N * (2,1))) * (N * (3,2)))) by MATRIX_9: 46;

      hence thesis;

    end;

    theorem :: MATRIXR2:39

    for f be Permutation of ( Seg 0 ) holds f = ( <*> NAT );

    

     Lm4: ( idseq 0 ) is Permutation of ( Seg 0 ) by FINSEQ_2: 55;

    theorem :: MATRIXR2:40

    

     Th40: ( Permutations 0 ) = {( <*> NAT )}

    proof

      now

        let p be object;

        assume p in ( Permutations 0 );

        then

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

        q = ( <*> NAT );

        hence p in {( <*> NAT )} by TARSKI:def 1;

      end;

      then

       A1: ( Permutations 0 ) c= {( <*> NAT )};

       {( <*> NAT )} c= ( Permutations 0 )

      proof

        let x be object;

        assume x in {( <*> NAT )};

        then x is Permutation of ( Seg 0 ) by Lm4, TARSKI:def 1;

        hence thesis by MATRIX_1:def 12;

      end;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: MATRIXR2:41

    

     Th41: for K be Ring holds for A be Matrix of 0 , K holds ( Det A) = ( 1. K)

    proof

      let K be Ring;

      reconsider kk = ( idseq 0 ) as Element of ( Permutations 0 ) by Th40, TARSKI:def 1;

      let A be Matrix of 0 , K;

      

       A1: (( Path_product A) . ( idseq 0 )) = ( 1. K)

      proof

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

        

         A2: ( - (( 1_ K),p)) = ( 1_ K)

        proof

          reconsider q = ( id ( Seg 0 )) as Element of ( Permutations 0 ) by Lm4, MATRIX_1:def 12;

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

          then q is even by MATRIX_1: 16;

          hence thesis by MATRIX_1:def 16;

        end;

        ( 1_ K) is_a_unity_wrt the multF of K by GROUP_1: 21;

        then ( len ( Path_matrix (p,A))) = 0 & the multF of K is having_a_unity by MATRIX_3:def 7, SETWISEO:def 2;

        

        then (the multF of K $$ ( Path_matrix (p,A))) = ( the_unity_wrt the multF of K) by FINSOP_1:def 1

        .= ( 1_ K) by GROUP_1: 22;

        hence thesis by A2, MATRIX_3:def 8;

      end;

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

      

      then

       A3: ( In (( Permutations 0 ),( Fin ( Permutations 0 )))) = ( Permutations 0 ) by SUBSET_1:def 8

      .= {.kk.} by Th40;

      ( Det A) = (the addF of K $$ (( In (( Permutations 0 ),( Fin ( Permutations 0 )))),( Path_product A))) by MATRIX_3:def 9

      .= ( 1. K) by A1, A3, SETWISEO: 17;

      hence thesis;

    end;

    theorem :: MATRIXR2:42

    for A be Matrix of 0 , REAL holds ( Det A) = 1

    proof

      let A be Matrix of 0 , REAL ;

      

      thus ( Det A) = ( 1. F_Real ) by Th41

      .= 1;

    end;

    theorem :: MATRIXR2:43

    

     Th43: for n be Nat, A be Matrix of n, K holds ( Det A) = ( Det (A @ ))

    proof

      let n be Nat, A be Matrix of n, K;

      n = 0 or n >= 1 & n is Nat by NAT_1: 14;

      then ( Det A) = ( 1_ K) & ( Det (A @ )) = ( 1_ K) or ( Det A) = ( Det (A @ )) by Th41, MATRIX_7: 37;

      hence thesis;

    end;

    theorem :: MATRIXR2:44

    for A be Matrix of n, REAL holds ( Det A) = ( Det (A @ )) by Th43;

    theorem :: MATRIXR2:45

    

     Th45: for A,B be Matrix of n, K holds ( Det (A * B)) = (( Det A) * ( Det B))

    proof

      let A,B be Matrix of n, K;

      per cases ;

        suppose n > 0 ;

        hence thesis by MATRIX11: 62;

      end;

        suppose n <= 0 ;

        then

         A1: n = 0 ;

        

        hence ( Det (A * B)) = ( 1. K) by Th41

        .= (( 1. K) * ( 1. K))

        .= (( Det A) * ( 1. K)) by A1, Th41

        .= (( Det A) * ( Det B)) by A1, Th41;

      end;

    end;

    theorem :: MATRIXR2:46

    

     Th46: for A,B be Matrix of n, REAL holds ( Det (A * B)) = (( Det A) * ( Det B))

    proof

      set K = F_Real ;

      let A,B be Matrix of n, REAL ;

      reconsider Na = ( MXR2MXF A), Nb = ( MXR2MXF B) as Matrix of n, K;

      ( Det (A * B)) = (( Det Na) * ( Det Nb)) by Th45

      .= (( Det A) * ( Det B));

      hence thesis;

    end;

    begin

    theorem :: MATRIXR2:47

    for x,y be FinSequence of REAL , A be Matrix of REAL st ( len x) = ( len A) & ( len y) = ( len x) & ( len x) > 0 holds ((x - y) * A) = ((x * A) - (y * A))

    proof

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

      assume that

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

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

       A3: ( len x) > 0 ;

      

       A4: ( width ( LineVec2Mx y)) = ( len y) by MATRIXR1:def 10;

      

       A5: ( width ( LineVec2Mx x)) = ( len x) by MATRIXR1:def 10;

      

      then

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

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

      

       A7: ( len ( LineVec2Mx y)) = 1 by MATRIXR1:def 10;

      

       A8: ( len ( LineVec2Mx x)) = 1 by MATRIXR1:def 10;

      then

       A9: 1 <= ( len (( LineVec2Mx x) * A)) by A1, A5, MATRIX_3:def 4;

      

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

      .= ( len ( LineVec2Mx y)) by A7, MATRIXR1:def 10

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

      

      thus ((x - y) * A) = ( Line (((( LineVec2Mx x) - ( LineVec2Mx y)) * A),1)) by A2, Th23

      .= ( Line (((( LineVec2Mx x) * A) - (( LineVec2Mx y) * A)),1)) by A1, A2, A3, A5, A4, A8, A7, Th16

      .= ((x * A) - (y * A)) by A6, A10, A9, Th25;

    end;

    theorem :: MATRIXR2:48

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

    proof

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

      assume that

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

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

       A3: ( len x) > 0 and

       A4: ( len A) > 0 ;

      

       A5: ( len ( ColVec2Mx y)) = ( len y) by A2, A3, MATRIXR1:def 9;

      

       A6: ( width ( ColVec2Mx y)) = 1 by A2, A3, MATRIXR1:def 9;

      

       A7: ( len ( ColVec2Mx x)) = ( len x) by A3, MATRIXR1:def 9;

      

      then

       A8: ( len (A * ( ColVec2Mx x))) = ( len A) by A1, MATRIX_3:def 4

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

      

       A9: ( width ( ColVec2Mx x)) = 1 by A3, MATRIXR1:def 9;

      then

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

      

       A11: ( width (A * ( ColVec2Mx x))) = ( width ( ColVec2Mx x)) by A1, A7, MATRIX_3:def 4

      .= ( width ( ColVec2Mx y)) by A3, A6, MATRIXR1:def 9

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

      

      thus (A * (x - y)) = ( Col ((A * (( ColVec2Mx x) - ( ColVec2Mx y))),1)) by A2, A3, Th24

      .= ( Col (((A * ( ColVec2Mx x)) - (A * ( ColVec2Mx y))),1)) by A1, A2, A3, A4, A7, A5, A9, A6, Th20

      .= ((A * x) - (A * y)) by A8, A11, A10, Th26;

    end;

    theorem :: MATRIXR2:49

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

    proof

      let 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, MATRIXR1: 52;

      

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

      then

       A6: ((A @ ) * ( - x)) = (( - 1) * ((A @ ) * x)) by A2, MATRIXR1: 59;

      

       A7: ( len ( - x)) = ( len x) by RVSUM_1: 114;

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

      then (( - x) * ((A @ ) @ )) = ((A @ ) * ( - x)) by A2, A5, A7, MATRIXR1: 53;

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

    end;

    theorem :: MATRIXR2:50

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

    proof

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

      assume that

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

       A2: ( len x) > 0 ;

      

       A3: ( len ( ColVec2Mx x)) = ( len x) by A2, MATRIXR1:def 9;

      ( width ( ColVec2Mx x)) = 1 by A2, MATRIXR1:def 9;

      then

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

      

      thus (A * ( - x)) = ( Col ((A * (( - 1) * ( ColVec2Mx x))),1)) by A2, MATRIXR1: 47

      .= ( Col ((( - 1) * (A * ( ColVec2Mx x))),1)) by A1, A3, MATRIXR1: 40

      .= ( - (A * x)) by A4, MATRIXR1: 56;

    end;

    theorem :: MATRIXR2:51

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

    proof

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

      assume that

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

       A2: ( len x) > 0 ;

      

       A3: ( width A) = ( len (x * A)) by A1, MATRIXR1: 62;

      

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

      then

       A5: ( len (x * ( - A))) = ( width A) by A1, MATRIXR1: 62;

      ((x * ( - A)) + (x * A)) = (x * (( - A) + A)) by A1, A2, A4, MATRIXR1: 64

      .= (x * ( 0_Rmatrix (( len A),( width A)))) by Th31

      .= ( 0* ( width A)) by A1, A2, MATRIXR1: 66;

      hence thesis by A5, A3, Th1;

    end;

    theorem :: MATRIXR2:52

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

    proof

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

      assume that

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

       A2: ( len A) > 0 and

       A3: ( len x) > 0 ;

      

       A4: ( len ( ColVec2Mx x)) = ( len x) & ( width ( ColVec2Mx x)) = 1 by A3, MATRIXR1:def 9;

      then

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

      

      thus (( - A) * x) = ( Col (((( - 1) * A) * ( ColVec2Mx x)),1)) by Th9

      .= ( Col ((( - 1) * (A * ( ColVec2Mx x))),1)) by A1, A2, A3, A4, MATRIXR1: 41

      .= ( - (A * x)) by A5, MATRIXR1: 56;

    end;

    theorem :: MATRIXR2:53

    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, MATRIXR1:def 9;

      ( width ( ColVec2Mx x)) = 1 by A2, MATRIXR1:def 9;

      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, MATRIXR1: 47

      .= ( Col ((a * (A * ( ColVec2Mx x))),1)) by A1, A3, MATRIXR1: 40

      .= (a * (A * x)) by A4, MATRIXR1: 56;

    end;

    theorem :: MATRIXR2:54

    for x be FinSequence of REAL , A,B be Matrix of REAL st ( len x) = ( len A) & ( len A) = ( len B) & ( width A) = ( width B) & ( len A) > 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 x) = ( len A) and

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

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

       A4: ( len A) > 0 ;

      

       A5: ( width ( LineVec2Mx x)) = ( len x) by MATRIXR1:def 10;

      

      then

       A6: ( len (( LineVec2Mx x) * A)) = ( len ( LineVec2Mx x)) by A1, MATRIX_3:def 4

      .= 1 by MATRIXR1:def 10;

      

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

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

      

       A8: ( width (( LineVec2Mx x) * A)) = ( width A) by A1, A5, MATRIX_3:def 4

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

      ( len ( LineVec2Mx x)) = 1 by MATRIXR1:def 10;

      

      hence (x * (A - B)) = ( Line (((( LineVec2Mx x) * A) - (( LineVec2Mx x) * B)),1)) by A1, A2, A3, A4, A5, Th20

      .= ((x * A) - (x * B)) by A8, A7, A6, Th25;

    end;

    theorem :: MATRIXR2:55

    for x be FinSequence of REAL , A,B be Matrix of REAL st ( len x) = ( width A) & ( len A) = ( len B) & ( width A) = ( width B) & ( len x) > 0 & ( len A) > 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 x) = ( width A) and

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

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

       A4: ( len x) > 0 and

       A5: ( len A) > 0 ;

      

       A6: ( len ( ColVec2Mx x)) = ( len x) by A4, MATRIXR1:def 9;

      

      then

       A7: ( len (A * ( ColVec2Mx x))) = ( len A) by A1, MATRIX_3:def 4

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

      

       A8: ( width (A * ( ColVec2Mx x))) = ( width ( ColVec2Mx x)) by A1, A6, MATRIX_3:def 4

      .= 1 by A4, MATRIXR1: 45;

      

       A9: ( width (A * ( ColVec2Mx x))) = ( width ( ColVec2Mx x)) by A1, A6, MATRIX_3:def 4

      .= ( width (B * ( ColVec2Mx x))) by A1, A3, A6, MATRIX_3:def 4;

      

      thus ((A - B) * x) = ( Col (((A * ( ColVec2Mx x)) - (B * ( ColVec2Mx x))),1)) by A1, A2, A3, A4, A5, A6, Th16

      .= ((A * x) - (B * x)) by A7, A9, A8, Th26;

    end;

    theorem :: MATRIXR2:56

    

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

    proof

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

      

       A1: ( len ( LineVec2Mx (x * A))) = 1 by MATRIXR1:def 10;

      assume

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

      then

       A3: ( width ( MXR2MXF ( LineVec2Mx x))) = ( len ( MXR2MXF A)) by MATRIXR1:def 10;

      ( width ( LineVec2Mx (x * A))) = ( len (x * A)) by MATRIXR1:def 10;

      then

       A4: ( width ( LineVec2Mx (x * A))) = ( width A) by A2, MATRIXR1: 62;

      

       A5: ( len (x * A)) = ( width A) by A2, MATRIXR1: 62;

      then

       A6: ( width ( MXR2MXF ( LineVec2Mx (x * A)))) = ( width ( MXR2MXF A)) by MATRIXR1:def 10;

      

       A7: ( width ( LineVec2Mx x)) = ( len x) by MATRIXR1:def 10;

      

       A8: for i,j be Nat st [i, j] in ( Indices ( MXR2MXF ( LineVec2Mx (x * A)))) holds (( MXR2MXF ( LineVec2Mx (x * A))) * (i,j)) = (( Line (( MXR2MXF ( LineVec2Mx x)),i)) "*" ( Col (( MXR2MXF A),j)))

      proof

        ( len (( MXR2MXF ( LineVec2Mx x)) * ( MXR2MXF A))) = ( len ( MXR2MXF ( LineVec2Mx x))) by A3, MATRIX_3:def 4;

        then ( len (( MXR2MXF ( LineVec2Mx x)) * ( MXR2MXF A))) = 1 by MATRIXR1:def 10;

        then

         A9: 1 in ( Seg ( len (( MXR2MXF ( LineVec2Mx x)) * ( MXR2MXF A))));

        let i,j be Nat;

        

         A10: ( width (( LineVec2Mx x) * A)) = ( width A) by A2, A7, MATRIX_3:def 4;

        assume

         A11: [i, j] in ( Indices ( MXR2MXF ( LineVec2Mx (x * A))));

        then

         A12: j in ( Seg ( width A)) by A4, ZFMISC_1: 87;

        then j in ( dom (x * A)) by A5, FINSEQ_1:def 3;

        then

         A13: (( Line ((( LineVec2Mx x) * A),1)) . j) = (( LineVec2Mx (x * A)) * (1,j)) by MATRIXR1:def 10;

        ( Indices ( LineVec2Mx (x * A))) = [:( Seg 1), ( Seg ( width A)):] by A1, A4, FINSEQ_1:def 3;

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

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

        then

         A14: i = 1 by XXREAL_0: 1;

        ( width (( MXR2MXF ( LineVec2Mx x)) * ( MXR2MXF A))) = ( width A) by A3, MATRIX_3:def 4;

        then [1, j] in [:( Seg ( len (( MXR2MXF ( LineVec2Mx x)) * ( MXR2MXF A)))), ( Seg ( width (( MXR2MXF ( LineVec2Mx x)) * ( MXR2MXF A)))):] by A12, A9, ZFMISC_1: 87;

        then

         A15: [1, j] in ( Indices (( MXR2MXF ( LineVec2Mx x)) * ( MXR2MXF A))) by FINSEQ_1:def 3;

        ( width ( MXR2MXF ( LineVec2Mx x))) = ( len ( MXR2MXF A)) by A2, MATRIXR1:def 10;

        then ((( LineVec2Mx x) * A) * (1,j)) = (( Line (( MXR2MXF ( LineVec2Mx x)),i)) "*" ( Col (( MXR2MXF A),j))) by A14, A15, MATRIX_3:def 4;

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

      end;

      ( len ( MXR2MXF ( LineVec2Mx (x * A)))) = ( len ( MXR2MXF ( LineVec2Mx x))) by A1, MATRIXR1:def 10;

      hence thesis by A6, A3, A8, MATRIX_3:def 4;

    end;

    theorem :: MATRIXR2:57

    

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

    proof

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

      assume that

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

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

      ( width ( LineVec2Mx x)) = ( len x) by MATRIXR1:def 10;

      

      hence (x * (A * B)) = ( Line (((( LineVec2Mx x) * A) * B),1)) by A1, A2, MATRIX_3: 33

      .= ((x * A) * B) by A1, Th56;

    end;

    theorem :: MATRIXR2:58

    

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

    proof

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

      assume that

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

       A2: ( len x) > 0 and

       A3: ( len A) > 0 ;

      

       A4: ( len ( ColVec2Mx x)) = ( len x) by A2, MATRIXR1:def 9;

      

       A5: ( len ( MXR2MXF ( ColVec2Mx x))) = ( width ( MXR2MXF A)) by A1, A2, MATRIXR1:def 9;

      

      then

       A6: ( width (( MXR2MXF A) * ( MXR2MXF ( ColVec2Mx x)))) = ( width ( ColVec2Mx x)) by MATRIX_3:def 4

      .= 1 by A2, MATRIXR1:def 9;

      

       A7: ( len (( MXR2MXF A) * ( MXR2MXF ( ColVec2Mx x)))) = ( len A) by A5, MATRIX_3:def 4;

      

       A8: ( len (A * x)) = ( len A) by A1, A2, MATRIXR1: 61;

      then

       A9: ( width ( ColVec2Mx (A * x))) = 1 by A3, MATRIXR1:def 9;

      

       A10: ( len ( ColVec2Mx (A * x))) = ( len A) by A3, A8, MATRIXR1:def 9;

      

       A11: ( len ( ColVec2Mx (A * x))) = ( len (A * x)) by A3, A8, MATRIXR1:def 9;

      

       A12: for i,j be Nat st [i, j] in ( Indices ( MXR2MXF ( ColVec2Mx (A * x)))) holds (( MXR2MXF ( ColVec2Mx (A * x))) * (i,j)) = (( Line (( MXR2MXF A),i)) "*" ( Col (( MXR2MXF ( ColVec2Mx x)),j)))

      proof

        let i,j be Nat;

        

         A13: 1 in ( Seg 1) & ( Indices ( ColVec2Mx (A * x))) = [:( Seg ( len ( ColVec2Mx (A * x)))), ( Seg 1):] by A9, FINSEQ_1:def 3;

        assume

         A14: [i, j] in ( Indices ( MXR2MXF ( ColVec2Mx (A * x))));

        then

         A15: j in ( Seg ( width (( MXR2MXF A) * ( MXR2MXF ( ColVec2Mx x))))) by A9, A6, ZFMISC_1: 87;

        

         A16: ( Indices ( ColVec2Mx (A * x))) = [:( Seg ( len A)), ( Seg 1):] by A8, A11, A9, FINSEQ_1:def 3;

        then

         A17: i in ( Seg ( len A)) by A14, ZFMISC_1: 87;

        then

         A18: i in ( dom (A * x)) by A8, FINSEQ_1:def 3;

        i in ( Seg ( len (( MXR2MXF A) * ( MXR2MXF ( ColVec2Mx x))))) by A7, A14, A16, ZFMISC_1: 87;

        then [i, j] in [:( Seg ( len (( MXR2MXF A) * ( MXR2MXF ( ColVec2Mx x))))), ( Seg ( width (( MXR2MXF A) * ( MXR2MXF ( ColVec2Mx x))))):] by A15, ZFMISC_1: 87;

        then

         A19: [i, j] in ( Indices (( MXR2MXF A) * ( MXR2MXF ( ColVec2Mx x)))) by FINSEQ_1:def 3;

        j in ( Seg 1) by A9, A14, ZFMISC_1: 87;

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

        then

         A20: j = 1 by XXREAL_0: 1;

        i in ( Seg ( len ( ColVec2Mx (A * x)))) by A10, A14, A16, ZFMISC_1: 87;

        then [i, 1] in ( Indices ( ColVec2Mx (A * x))) by A13, ZFMISC_1: 87;

        then

         A21: ex p2 be FinSequence of REAL st p2 = (( ColVec2Mx (A * x)) . i) & (( ColVec2Mx (A * x)) * (i,1)) = (p2 . 1) by MATRIX_0:def 5;

        

         A22: (( Col ((A * ( ColVec2Mx x)),1)) . i) = ( <*((A * x) . i)*> . 1) by FINSEQ_1: 40

        .= (( ColVec2Mx (A * x)) * (i,1)) by A3, A8, A18, A21, MATRIXR1:def 9;

        ( len (A * ( ColVec2Mx x))) = ( len A) by A1, A4, MATRIX_3:def 4;

        then i in ( dom (A * ( ColVec2Mx x))) by A17, FINSEQ_1:def 3;

        then (( Col ((A * ( ColVec2Mx x)),1)) . i) = ((A * ( ColVec2Mx x)) * (i,j)) by A20, MATRIX_0:def 8;

        hence thesis by A5, A20, A22, A19, MATRIX_3:def 4;

      end;

      

       A23: ( len ( MXR2MXF ( ColVec2Mx (A * x)))) = ( len ( MXR2MXF A)) by A3, A8, MATRIXR1:def 9;

      ( width ( MXR2MXF ( ColVec2Mx (A * x)))) = 1 by A3, A8, MATRIXR1:def 9

      .= ( width ( MXR2MXF ( ColVec2Mx x))) by A2, MATRIXR1:def 9;

      hence thesis by A23, A5, A12, MATRIX_3:def 4;

    end;

    theorem :: MATRIXR2:59

    

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

    proof

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

      assume that

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

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

       A3: ( len x) > 0 and

       A4: ( len B) > 0 ;

      ( len ( ColVec2Mx x)) = ( len x) by A3, MATRIXR1:def 9;

      

      hence ((A * B) * x) = ( Col ((A * (B * ( ColVec2Mx x))),1)) by A1, A2, MATRIX_3: 33

      .= (A * (B * x)) by A1, A3, A4, Th58;

    end;

    theorem :: MATRIXR2:60

    for B be Matrix of n, m, REAL , A be Matrix of m, k, REAL st n > 0 holds (for i, j st [i, j] in ( Indices (B * A)) holds ((B * A) * (i,j)) = ((( Line (B,i)) * A) . j))

    proof

      let B be Matrix of n, m, REAL , A be Matrix of m, k, REAL ;

      assume

       A1: n > 0 ;

      then

       A2: ( width B) = m by MATRIX_0: 23;

      let i, j;

      

       A3: ( len A) = m by MATRIX_0:def 2;

      then

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

      assume

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

      then

       A6: j in ( Seg ( width (B * A))) by ZFMISC_1: 87;

      ( width B) = ( len A) by A1, A3, MATRIX_0: 23;

      then

       A7: ((B * A) * (i,j)) = (( Line (B,i)) "*" ( Col (A,j))) by A5, MATRPROB: 39;

      ( width A) = ( width (B * A)) by A3, A2, MATRPROB: 39;

      then j in ( Seg ( len (( Line (B,i)) * A))) by A6, A4, MATRIXR1: 62;

      hence thesis by A7, A4, MATRPROB: 40;

    end;

    theorem :: MATRIXR2:61

    

     Th61: for A,B be Matrix of n, REAL holds for i, j st [i, j] in ( Indices (B * A)) holds ((B * A) * (i,j)) = ((( Line (B,i)) * A) . j)

    proof

      let A,B be Matrix of n, REAL ;

      let i, j;

      assume

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

      then

       A2: j in ( Seg ( width (B * A))) by ZFMISC_1: 87;

      

       A3: ( len A) = n by MATRIX_0:def 2;

      then ( width B) = ( len A) by MATRIX_0: 24;

      then

       A4: ((B * A) * (i,j)) = (( Line (B,i)) "*" ( Col (A,j))) by A1, MATRPROB: 39;

      

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

      then

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

      ( width A) = ( width (B * A)) by A3, A5, MATRPROB: 39;

      then j in ( Seg ( len (( Line (B,i)) * A))) by A2, A6, MATRIXR1: 62;

      hence thesis by A4, A6, MATRPROB: 40;

    end;

    theorem :: MATRIXR2:62

    for A,B be Matrix of n, REAL st n > 0 holds for i, j st [i, j] in ( Indices (A * B)) holds ((A * B) * (i,j)) = ((A * ( Col (B,j))) . i)

    proof

      let A,B be Matrix of n, REAL ;

      assume

       A1: n > 0 ;

      let i, j;

      

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

      assume

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

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

      then

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

      

       A5: ( len B) = n by MATRIX_0:def 2;

      then

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

      ( width A) = ( len B) by A5, MATRIX_0: 24;

      then

       A7: ((A * B) * (i,j)) = (( Line (A,i)) "*" ( Col (B,j))) by A3, MATRPROB: 39;

      ( len (A * B)) = n & ( len A) = n by MATRIX_0: 24;

      then i in ( Seg ( len (A * ( Col (B,j))))) by A1, A4, A2, A6, MATRIXR1: 61;

      hence thesis by A1, A2, A7, A6, MATRPROB: 41;

    end;

    begin

    definition

      let n be Nat;

      :: MATRIXR2:def2

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

      correctness ;

    end

    theorem :: MATRIXR2:63

    

     Th63: (for i st [i, i] in ( Indices ( 1_Rmatrix n)) holds (( 1_Rmatrix n) * (i,i)) = 1) & for i, j st [i, j] in ( Indices ( 1_Rmatrix n)) & i <> j holds (( 1_Rmatrix n) * (i,j)) = 0

    proof

      set K = F_Real ;

      thus for i st [i, i] in ( Indices ( 1_Rmatrix n)) holds (( 1_Rmatrix n) * (i,i)) = 1

      proof

        let i;

        assume [i, i] in ( Indices ( 1_Rmatrix n));

        

        hence (( 1_Rmatrix n) * (i,i)) = ( 1_ F_Real ) by MATRIX_1:def 3

        .= 1;

      end;

      let i, j;

      assume [i, j] in ( Indices ( 1_Rmatrix n)) & i <> j;

      

      hence (( 1_Rmatrix n) * (i,j)) = ( 0. K) by MATRIX_1:def 3

      .= 0 ;

    end;

    theorem :: MATRIXR2:64

    

     Th64: (( 1_Rmatrix n) @ ) = ( 1_Rmatrix n)

    proof

      per cases ;

        suppose

         A1: n > 0 ;

        

         A2: ( len ( 1_Rmatrix n)) = n by MATRIX_0: 24;

        

         A3: ( Indices ( 1_Rmatrix n)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

        

         A4: for i,j be Nat st [i, j] in ( Indices ( 1_Rmatrix n)) holds (( 1_Rmatrix n) * (i,j)) = ((( 1_Rmatrix n) @ ) * (i,j))

        proof

          let i,j be Nat;

          reconsider i0 = i, j0 = j as Nat;

          assume

           A5: [i, j] in ( Indices ( 1_Rmatrix n));

          then i in ( Seg n) & j in ( Seg n) by A3, ZFMISC_1: 87;

          then

           A6: [j, i] in ( Indices ( 1_Rmatrix n)) by A3, ZFMISC_1: 87;

          per cases ;

            suppose i = j;

            hence thesis by A5, MATRIX_0:def 6;

          end;

            suppose i <> j;

            then (( 1_Rmatrix n) * (i0,j0)) = 0 & (( 1_Rmatrix n) * (j0,i0)) = 0 by A5, A6, Th63;

            hence thesis by A6, MATRIX_0:def 6;

          end;

        end;

        

         A7: ( width ( 1_Rmatrix n)) = n by MATRIX_0: 24;

        then ( len (( 1_Rmatrix n) @ )) = ( width ( 1_Rmatrix n)) & ( width (( 1_Rmatrix n) @ )) = ( len ( 1_Rmatrix n)) by A1, MATRIX_0: 54;

        hence thesis by A7, A2, A4, MATRIX_0: 21;

      end;

        suppose n = 0 ;

        hence thesis by MATRIX_0: 45;

      end;

    end;

    theorem :: MATRIXR2:65

    

     Th65: for n,m be Nat st n > 0 holds (( 0_Rmatrix (n,m)) + ( 0_Rmatrix (n,m))) = ( 0_Rmatrix (n,m))

    proof

      let n,m be Nat;

      assume

       A1: n > 0 ;

      then ( width ( 0_Rmatrix (n,m))) = m & ( len ( 0_Rmatrix (n,m))) = n by MATRIX_0: 23;

      then (( 0 + 0 ) * ( 0_Rmatrix (n,m))) = ( 0_Rmatrix (n,m)) by A1, MATRIXR1: 44;

      hence thesis by Th12;

    end;

    theorem :: MATRIXR2:66

    for a be Real st n > 0 holds (a * ( 0_Rmatrix (n,m))) = ( 0_Rmatrix (n,m))

    proof

      let a be Real;

      

       A1: ( len (a * ( 0_Rmatrix (n,m)))) = ( len ( 0_Rmatrix (n,m))) & ( width (a * ( 0_Rmatrix (n,m)))) = ( width ( 0_Rmatrix (n,m))) by MATRIXR1: 27;

      assume

       A2: n > 0 ;

      then

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

      (a * ( 0_Rmatrix (n,m))) = (a * (( 0_Rmatrix (n,m)) + ( 0_Rmatrix (n,m)))) by A2, Th65

      .= ((a * ( 0_Rmatrix (n,m))) + (a * ( 0_Rmatrix (n,m)))) by A3, MATRIXR1: 43;

      hence thesis by A3, A1, MATRIXR1: 37;

    end;

    theorem :: MATRIXR2:67

    

     Th67: for K be Field, A be Matrix of K holds (A * ( 1. (K,( width A)))) = A

    proof

      let K be Field, A be Matrix of K;

      set n = ( width A);

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

      

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

      

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

      then

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

       A4:

      now

        let i,j be Nat;

        assume

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

        then

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

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

        then

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

         A8:

        now

          let k be Nat;

          assume that

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

           A10: k <> j;

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

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

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

          then [k, j] in ( Indices B) by A6, ZFMISC_1: 87;

          hence (( Col (B,j)) . k) = ( 0. K) by A10, MATRIX_3: 16;

        end;

        

         A11: j in ( Seg ( width A)) by A1, A3, A5, ZFMISC_1: 87;

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

        then [j, j] in ( Indices B) by A1, A11, ZFMISC_1: 87;

        then

         A12: (( Col (B,j)) . j) = ( 1_ K) by MATRIX_3: 16;

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

        then

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

        

        thus ((A * B) * (i,j)) = (( Line (A,i)) "*" ( Col (B,j))) by A2, A5, MATRIX_3:def 4

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

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

        .= (( Line (A,i)) . j) by A13, A7, A8, A12, MATRIX_3: 17

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

      end;

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

      hence thesis by A1, A3, A4, MATRIX_0: 21;

    end;

    theorem :: MATRIXR2:68

    

     Th68: for A be Matrix of K holds (( 1. (K,( len A))) * A) = A

    proof

      let A be Matrix of K;

      set n = ( len A);

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

      

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

      

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

      then

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

       A4:

      now

        

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

        let i,j be Nat;

        assume

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

        

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

        then

         A8: i in ( Seg ( width B)) by A1, A2, A3, A6, ZFMISC_1: 87;

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

        then

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

        

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

        then

         A11: i in ( dom B) by A3, A6, A7, ZFMISC_1: 87;

        then [i, i] in ( Indices B) by A8, ZFMISC_1: 87;

        then

         A12: (( Line (B,i)) . i) = ( 1_ K) by MATRIX_3: 15;

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

        then

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

         A14:

        now

          let k be Nat;

          assume that

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

           A16: k <> i;

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

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

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

          hence (( Line (B,i)) . k) = ( 0. K) by A16, MATRIX_3: 15;

        end;

        

        thus ((B * A) * (i,j)) = (( Line (B,i)) "*" ( Col (A,j))) by A2, A6, MATRIX_3:def 4

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

        .= (( Col (A,j)) . i) by A9, A13, A14, A12, MATRIX_3: 17

        .= (A * (i,j)) by A1, A5, A10, A11, MATRIX_0:def 8;

      end;

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

      hence thesis by A1, A3, A4, MATRIX_0: 21;

    end;

    theorem :: MATRIXR2:69

    for A be Matrix of REAL holds (n = ( width A) implies (A * ( 1_Rmatrix n)) = A) & (m = ( len A) implies (( 1_Rmatrix m) * A) = A) by Th67, Th68;

    theorem :: MATRIXR2:70

    

     Th70: for A be Matrix of n, REAL holds (( 1_Rmatrix n) * A) = A

    proof

      let A be Matrix of n, REAL ;

      n = ( len A) by MATRIX_0:def 2;

      hence thesis by Th68;

    end;

    theorem :: MATRIXR2:71

    

     Th71: for A be Matrix of n, REAL holds (A * ( 1_Rmatrix n)) = A

    proof

      let A be Matrix of n, REAL ;

      

       A1: n = ( len A) by MATRIX_0:def 2;

      now

        per cases ;

          case n <> 0 ;

          hence n = ( width A) by A1, MATRIX_0: 20;

        end;

          case n = 0 ;

          hence n = ( width A) by A1, MATRIX_0:def 3;

        end;

      end;

      hence thesis by Th67;

    end;

    theorem :: MATRIXR2:72

    

     Th72: ( Det ( 1_Rmatrix n)) = 1

    proof

      per cases ;

        suppose n >= 1;

        

        hence ( Det ( 1_Rmatrix n)) = ( 1_ F_Real ) by MATRIX_7: 16

        .= 1;

      end;

        suppose n < 1;

        then n = 0 by NAT_1: 25;

        

        hence ( Det ( 1_Rmatrix n)) = ( 1. F_Real ) by Th41

        .= 1;

      end;

    end;

    definition

      let n be Nat;

      :: MATRIXR2:def3

      func 0_Rmatrix (n) -> Matrix of n, REAL equals ( 0_Rmatrix (n,n));

      correctness ;

    end

    theorem :: MATRIXR2:73

    n > 0 implies ( Det ( 0_Rmatrix n)) = 0

    proof

      set K = F_Real ;

      assume n > 0 ;

      then n >= ( 0 + 1) by NAT_1: 13;

      

      then ( Det ( 0_Rmatrix n)) = ( 0. K) by MATRIX_7: 15

      .= 0 ;

      hence thesis;

    end;

    definition

      let n,i be Nat;

      :: MATRIXR2:def4

      func Base_FinSeq (n,i) -> FinSequence of REAL equals ((n |-> 0 ) +* (i,1));

      coherence

      proof

        reconsider n as Nat;

        ((n |-> 0 ) +* (i,1)) = ( Replace ((n |-> ( In ( 0 , REAL ))),i,( In (1, REAL ))));

        hence thesis;

      end;

    end

    reserve n,i,j for Nat;

    theorem :: MATRIXR2:74

    

     Th74: ( len ( Base_FinSeq (n,i))) = n

    proof

      ( len ((n |-> 0 ) +* (i,1))) = ( len (n |-> 0 )) by FUNCT_7: 97

      .= n by CARD_1:def 7;

      hence thesis;

    end;

    theorem :: MATRIXR2:75

    

     Th75: 1 <= i & i <= n implies (( Base_FinSeq (n,i)) . i) = 1

    proof

      

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

      assume 1 <= i & i <= n;

      then i in ( dom (n |-> 0 )) by A1, FINSEQ_3: 25;

      hence thesis by FUNCT_7: 31;

    end;

    theorem :: MATRIXR2:76

    

     Th76: 1 <= j & j <= n & i <> j implies (( Base_FinSeq (n,i)) . j) = 0

    proof

      assume that

       A1: 1 <= j & j <= n and

       A2: i <> j;

      

       A3: j in ( Seg n) by A1;

      

      thus (( Base_FinSeq (n,i)) . j) = ((n |-> 0 ) . j) by A2, FUNCT_7: 32

      .= 0 by A3, FINSEQ_2: 57;

    end;

    reserve n for Nat;

    theorem :: MATRIXR2:77

    ( Base_FinSeq (1,1)) = <*1*> & ( Base_FinSeq (2,1)) = <*1, 0 *> & ( Base_FinSeq (2,2)) = <* 0 , 1*> & ( Base_FinSeq (3,1)) = <*1, 0 , 0 *> & ( Base_FinSeq (3,2)) = <* 0 , 1, 0 *> & ( Base_FinSeq (3,3)) = <* 0 , 0 , 1*>

    proof

      

      thus ( Base_FinSeq (1,1)) = ( Replace ( <*( In ( 0 , REAL ))*>,1,( In (1, REAL )))) by FINSEQ_2: 59

      .= <*1*> by FINSEQ_7: 12;

      

      thus ( Base_FinSeq (2,1)) = ( Replace ( <*( In ( 0 , REAL )), ( In ( 0 , REAL ))*>,1,( In (1, REAL )))) by FINSEQ_2: 61

      .= <*1, 0 *> by FINSEQ_7: 13;

      

      thus ( Base_FinSeq (2,2)) = ( Replace ( <*( In ( 0 , REAL )), ( In ( 0 , REAL ))*>,2,( In (1, REAL )))) by FINSEQ_2: 61

      .= <* 0 , 1*> by FINSEQ_7: 14;

      

      thus ( Base_FinSeq (3,1)) = ( Replace ( <* 0 , 0 , 0 *>,1,( In (1, REAL )))) by FINSEQ_2: 62

      .= <*1, 0 , 0 *> by FINSEQ_7: 15;

      

      thus ( Base_FinSeq (3,2)) = ( Replace ( <*( In ( 0 , REAL )), ( In ( 0 , REAL )), ( In ( 0 , REAL ))*>,2,( In (1, REAL )))) by FINSEQ_2: 62

      .= <* 0 , 1, 0 *> by FINSEQ_7: 16;

      

      thus ( Base_FinSeq (3,3)) = ( Replace ( <*( In ( 0 , REAL )), ( In ( 0 , REAL )), ( In ( 0 , REAL ))*>,3,( In (1, REAL )))) by FINSEQ_2: 62

      .= <* 0 , 0 , 1*> by FINSEQ_7: 17;

    end;

    theorem :: MATRIXR2:78

    

     Th78: 1 <= i & i <= n implies (( 1_Rmatrix n) . i) = ( Base_FinSeq (n,i))

    proof

      assume

       A1: 1 <= i & i <= n;

      then 1 <= n by XXREAL_0: 2;

      then

       A2: 1 in ( Seg n);

      i in ( Seg n) by A1;

      then [i, 1] in [:( Seg n), ( Seg n):] by A2, ZFMISC_1: 87;

      then [i, 1] in ( Indices ( 1. ( F_Real ,n))) by MATRIX_0: 24;

      then

      consider q be FinSequence of REAL such that

       A3: q = (( 1_Rmatrix n) . i) and (( 1_Rmatrix n) * (i,1)) = (q . 1) by MATRIX_0:def 5;

      ( len ( 1_Rmatrix n)) = n by MATRIX_0: 24;

      then i in ( dom ( 1_Rmatrix n)) by A1, FINSEQ_3: 25;

      then q in ( rng ( 1_Rmatrix n)) by A3, FUNCT_1:def 3;

      then

       A4: ( len q) = n by MATRIX_0:def 2;

      

       A5: for j be Nat st 1 <= j & j <= n holds (q . j) = (( Base_FinSeq (n,i)) . j)

      proof

        

         A6: i in ( Seg n) by A1;

        let j be Nat;

        assume

         A7: 1 <= j & j <= n;

        j in ( Seg n) by A7;

        then [i, j] in [:( Seg n), ( Seg n):] by A6, ZFMISC_1: 87;

        then

         A8: [i, j] in ( Indices ( 1. ( F_Real ,n))) by MATRIX_0: 24;

        then

         A9: ex q0 be FinSequence of REAL st q0 = (( 1_Rmatrix n) . i) & (( 1_Rmatrix n) * (i,j)) = (q0 . j) by MATRIX_0:def 5;

        per cases ;

          suppose

           A10: i = j;

          then (( 1. ( F_Real ,n)) * (i,i)) = ( 1_ F_Real ) by A8, MATRIX_1:def 3;

          hence thesis by A1, A3, A9, A10, Th75;

        end;

          suppose

           A11: i <> j;

          then (( 1. ( F_Real ,n)) * (i,j)) = ( 0. F_Real ) by A8, MATRIX_1:def 3;

          hence thesis by A3, A7, A9, A11, Th76;

        end;

      end;

      ( len ( Base_FinSeq (n,i))) = n by Th74;

      hence thesis by A3, A4, A5, FINSEQ_1: 14;

    end;

    begin

    definition

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

      :: MATRIXR2:def5

      attr A is invertible means ex B be Matrix of n, REAL st (B * A) = ( 1_Rmatrix n) & (A * B) = ( 1_Rmatrix n);

    end

    definition

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

      assume

       A1: A is invertible;

      :: MATRIXR2:def6

      func Inv (A) -> Matrix of n, REAL means

      : Def6: (it * A) = ( 1_Rmatrix n) & (A * it ) = ( 1_Rmatrix n);

      existence by A1;

      uniqueness

      proof

        let B1,B2 be Matrix of n, REAL ;

        assume that (B1 * A) = ( 1_Rmatrix n) and

         A2: (A * B1) = ( 1_Rmatrix n) and

         A3: (B2 * A) = ( 1_Rmatrix n) and (A * B2) = ( 1_Rmatrix n);

        

         A4: ( len A) = n & ( width A) = n by MATRIX_0: 24;

        ( len B1) = n & ( width B2) = n by MATRIX_0: 24;

        then ((B2 * A) * B1) = (B2 * ( 1_Rmatrix n)) by A2, A4, MATRIX_3: 33;

        then B1 = (B2 * ( 1_Rmatrix n)) by A3, Th70;

        hence thesis by Th71;

      end;

    end

    registration

      let n;

      cluster ( 1_Rmatrix n) -> invertible;

      coherence

      proof

        (( 1_Rmatrix n) * ( 1_Rmatrix n)) = ( 1_Rmatrix n) by Th70;

        hence thesis;

      end;

    end

    theorem :: MATRIXR2:79

    ( Inv ( 1_Rmatrix n)) = ( 1_Rmatrix n)

    proof

      (( 1_Rmatrix n) * ( 1_Rmatrix n)) = ( 1_Rmatrix n) by Th70;

      hence thesis by Def6;

    end;

    theorem :: MATRIXR2:80

    

     Th80: for A,B1,B2 be Matrix of n, REAL st (B1 * A) = ( 1_Rmatrix n) & (A * B2) = ( 1_Rmatrix n) holds B1 = B2 & A is invertible

    proof

      let A,B1,B2 be Matrix of n, REAL ;

      assume that

       A1: (B1 * A) = ( 1_Rmatrix n) and

       A2: (A * B2) = ( 1_Rmatrix n);

      

       A3: ((B1 * A) * B2) = (B1 * (A * B2)) by Th28

      .= B1 by A2, Th71;

      hence B1 = B2 by A1, Th70;

      ((B1 * A) * B2) = B2 by A1, Th70;

      hence thesis by A1, A2, A3;

    end;

    theorem :: MATRIXR2:81

    for A be Matrix of n, REAL st A is invertible holds ( Det ( Inv A)) = (( Det A) " )

    proof

      let A be Matrix of n, REAL ;

      assume A is invertible;

      then (A * ( Inv A)) = ( 1_Rmatrix n) by Def6;

      then ( Det (A * ( Inv A))) = 1 by Th72;

      then

       A1: (( Det A) * ( Det ( Inv A))) = 1 by Th46;

      per cases ;

        suppose ( Det A) <> 0 ;

        hence thesis by A1, XCMPLX_0:def 7;

      end;

        suppose ( Det A) = 0 ;

        hence thesis by A1;

      end;

    end;

    theorem :: MATRIXR2:82

    for A be Matrix of n, REAL st A is invertible holds ( Det A) <> 0

    proof

      let A be Matrix of n, REAL ;

      assume A is invertible;

      then (A * ( Inv A)) = ( 1_Rmatrix n) by Def6;

      then ( Det (A * ( Inv A))) = 1 by Th72;

      then (( Det A) * ( Det ( Inv A))) = 1 by Th46;

      hence thesis;

    end;

    theorem :: MATRIXR2:83

    for A,B be Matrix of n, REAL st A is invertible & B is invertible holds (A * B) is invertible & ( Inv (A * B)) = (( Inv B) * ( Inv A))

    proof

      let A,B be Matrix of n, REAL ;

      assume that

       A1: A is invertible and

       A2: B is invertible;

      

       A3: ((( Inv B) * ( Inv A)) * (A * B)) = (((( Inv B) * ( Inv A)) * A) * B) by Th28

      .= ((( Inv B) * (( Inv A) * A)) * B) by Th28

      .= ((( Inv B) * ( 1_Rmatrix n)) * B) by A1, Def6

      .= (( Inv B) * B) by Th71

      .= ( 1_Rmatrix n) by A2, Def6;

      

       A4: ((A * B) * (( Inv B) * ( Inv A))) = (A * (B * (( Inv B) * ( Inv A)))) by Th28

      .= (A * ((B * ( Inv B)) * ( Inv A))) by Th28

      .= (A * (( 1_Rmatrix n) * ( Inv A))) by A2, Def6

      .= ((A * ( 1_Rmatrix n)) * ( Inv A)) by Th28

      .= (A * ( Inv A)) by Th71

      .= ( 1_Rmatrix n) by A1, Def6;

      hence (A * B) is invertible by A3;

      hence thesis by A3, A4, Def6;

    end;

    theorem :: MATRIXR2:84

    for A be Matrix of n, REAL st A is invertible holds ( Inv ( Inv A)) = A

    proof

      let A be Matrix of n, REAL ;

      assume A is invertible;

      then

       A1: (( Inv A) * A) = ( 1_Rmatrix n) & (A * ( Inv A)) = ( 1_Rmatrix n) by Def6;

      then ( Inv A) is invertible;

      hence thesis by A1, Def6;

    end;

    theorem :: MATRIXR2:85

    ( 1_Rmatrix 0 ) = ( 0_Rmatrix 0 ) & ( 1_Rmatrix 0 ) = {}

    proof

      

       A1: ( len ( 1_Rmatrix 0 )) = 0 by MATRIX_0: 24;

      ( len ( 0_Rmatrix 0 )) = 0 by MATRIX_0: 24;

      then ( 0_Rmatrix 0 ) = {} ;

      hence ( 1_Rmatrix 0 ) = ( 0_Rmatrix 0 ) by A1;

      thus thesis by A1;

    end;

    theorem :: MATRIXR2:86

    

     Th86: for x be FinSequence of REAL st ( len x) = n & n > 0 holds (( 1_Rmatrix n) * x) = x

    proof

      let x be FinSequence of REAL ;

      assume that

       A1: ( len x) = n and

       A2: n > 0 ;

      

       A3: ( len ( ColVec2Mx x)) = ( len x) by A1, A2, MATRIXR1:def 9;

      

       A4: ( len ( Col (( ColVec2Mx x),1))) = ( len ( ColVec2Mx x)) by MATRIX_0:def 8;

      

       A5: for k be Nat st 1 <= k & k <= ( len ( Col (( ColVec2Mx x),1))) holds (( Col (( ColVec2Mx x),1)) . k) = (x . k)

      proof

        let k be Nat;

        assume

         A6: 1 <= k & k <= ( len ( Col (( ColVec2Mx x),1)));

        

         A7: k in ( Seg ( len ( ColVec2Mx x))) by A4, A6;

        then

         A8: k in ( dom ( ColVec2Mx x)) by FINSEQ_1:def 3;

        then

         A9: (( Col (( ColVec2Mx x),1)) . k) = (( ColVec2Mx x) * (k,1)) by MATRIX_0:def 8;

        1 in ( Seg 1) & ( Indices ( ColVec2Mx x)) = [:( dom ( ColVec2Mx x)), ( Seg 1):] by A1, A2, MATRIXR1:def 9;

        then [k, 1] in ( Indices ( ColVec2Mx x)) by A8, ZFMISC_1: 87;

        then

        consider p be FinSequence of REAL such that

         A10: p = (( ColVec2Mx x) . k) and

         A11: (( ColVec2Mx x) * (k,1)) = (p . 1) by MATRIX_0:def 5;

        k in ( dom x) by A3, A7, FINSEQ_1:def 3;

        then p = <*(x . k)*> by A1, A2, A10, MATRIXR1:def 9;

        hence thesis by A9, A11, FINSEQ_1: 40;

      end;

      (( 1_Rmatrix n) * x) = ( Col (( MXF2MXR ( MXR2MXF ( ColVec2Mx x))),1)) by A1, A3, Th68

      .= x by A3, A4, A5;

      hence thesis;

    end;

    theorem :: MATRIXR2:87

    

     Th87: for n be Nat, x,y be FinSequence of REAL , A be Matrix of n, REAL st A is invertible & ( len x) = n & ( len y) = n & n > 0 holds (A * x) = y iff x = (( Inv A) * y)

    proof

      let n be Nat, x,y be FinSequence of REAL , A be Matrix of n, REAL ;

      assume that

       A1: A is invertible and

       A2: ( len x) = n and

       A3: ( len y) = n and

       A4: n > 0 ;

      

       A5: ( width A) = n & ( width ( Inv A)) = n by MATRIX_0: 24;

      

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

      thus (A * x) = y implies x = (( Inv A) * y)

      proof

        assume

         A7: (A * x) = y;

        

        thus x = (( 1_Rmatrix n) * x) by A2, A4, Th86

        .= ((( Inv A) * A) * x) by A1, Def6

        .= (( Inv A) * y) by A2, A4, A6, A5, A7, Th59;

      end;

      

       A8: ( len ( Inv A)) = n by MATRIX_0: 24;

      x = (( Inv A) * y) implies (A * x) = y

      proof

        assume

         A9: x = (( Inv A) * y);

        

        thus y = (( 1_Rmatrix n) * y) by A3, A4, Th86

        .= ((A * ( Inv A)) * y) by A1, Def6

        .= (A * x) by A3, A4, A8, A5, A9, Th59;

      end;

      hence thesis;

    end;

    theorem :: MATRIXR2:88

    

     Th88: for x be FinSequence of REAL st ( len x) = n holds (x * ( 1_Rmatrix n)) = x

    proof

      let x be FinSequence of REAL ;

      

       A1: ( width ( LineVec2Mx x)) = ( len x) by MATRIXR1:def 10;

      assume ( len x) = n;

      

      then (x * ( 1_Rmatrix n)) = ( Line (( MXF2MXR ( MXR2MXF ( LineVec2Mx x))),1)) by A1, Th67

      .= x by MATRIXR1: 48;

      hence thesis;

    end;

    theorem :: MATRIXR2:89

    

     Th89: for x,y be FinSequence of REAL , A be Matrix of n, REAL st A is invertible & ( len x) = n & ( len y) = n holds (x * A) = y iff x = (y * ( Inv A))

    proof

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

      assume that

       A1: A is invertible and

       A2: ( len x) = n and

       A3: ( len y) = n;

      

       A4: ( len A) = n & ( len ( Inv A)) = n by MATRIX_0: 24;

      

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

      thus (x * A) = y implies x = (y * ( Inv A))

      proof

        assume

         A6: (x * A) = y;

        

        thus x = (x * ( 1_Rmatrix n)) by A2, Th88

        .= (x * (A * ( Inv A))) by A1, Def6

        .= (y * ( Inv A)) by A2, A5, A4, A6, Th57;

      end;

      assume

       A7: x = (y * ( Inv A));

      

       A8: ( width ( Inv A)) = n by MATRIX_0: 24;

      

      thus y = (y * ( 1_Rmatrix n)) by A3, Th88

      .= (y * (( Inv A) * A)) by A1, Def6

      .= (x * A) by A3, A4, A8, A7, Th57;

    end;

    theorem :: MATRIXR2:90

    for A be Matrix of n, REAL st n > 0 & A is invertible holds for y be FinSequence of REAL st ( len y) = n holds ex x be FinSequence of REAL st ( len x) = n & (A * x) = y

    proof

      let A be Matrix of n, REAL ;

      assume that

       A1: n > 0 and

       A2: A is invertible;

      let y be FinSequence of REAL ;

      assume

       A3: ( len y) = n;

      reconsider x0 = (( Inv A) * y) as FinSequence of REAL ;

      ( len ( Inv A)) = n & ( width ( Inv A)) = n by MATRIX_0: 24;

      then

       A4: ( len x0) = n by A1, A3, MATRIXR1: 61;

      then (A * x0) = y by A1, A2, A3, Th87;

      hence thesis by A4;

    end;

    theorem :: MATRIXR2:91

    for A be Matrix of n, REAL st A is invertible holds for y be FinSequence of REAL st ( len y) = n holds ex x be FinSequence of REAL st ( len x) = n & (x * A) = y

    proof

      let A be Matrix of n, REAL ;

      assume

       A1: A is invertible;

      let y be FinSequence of REAL ;

      assume

       A2: ( len y) = n;

      reconsider x0 = (y * ( Inv A)) as FinSequence of REAL ;

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

      

      then

       A3: ( len x0) = ( width ( Inv A)) by A2, MATRIXR1: 62

      .= n by MATRIX_0: 24;

      then (x0 * A) = y by A1, A2, Th89;

      hence thesis by A3;

    end;

    theorem :: MATRIXR2:92

    for A be Matrix of n, REAL holds for x,y be FinSequence of REAL st ( len x) = n & ( len y) = n & (x * A) = y holds for j be Nat st 1 <= j & j <= n holds (y . j) = |(x, ( Col (A,j)))|

    proof

      let A be Matrix of n, REAL ;

      let x,y be FinSequence of REAL ;

      assume that

       A1: ( len x) = n and

       A2: ( len y) = n and

       A3: (x * A) = y;

      let j be Nat;

      assume 1 <= j & j <= n;

      then j in ( Seg ( len (x * A))) by A2, A3;

      hence thesis by A1, A3, MATRIX_0: 24, MATRPROB: 40;

    end;

    theorem :: MATRIXR2:93

    

     Th93: for A be Matrix of n, REAL st (for y be FinSequence of REAL st ( len y) = n holds (ex x be FinSequence of REAL st ( len x) = n & (x * A) = y)) holds ex B be Matrix of n, REAL st (B * A) = ( 1_Rmatrix n)

    proof

      let A be Matrix of n, REAL ;

      defpred P[ set, set] means for s be Nat, q be FinSequence of REAL st s = $1 & q = $2 holds ( len q) = n & (q * A) = ( Base_FinSeq (n,s));

      assume

       A1: for y be FinSequence of REAL st ( len y) = n holds ex x be FinSequence of REAL st ( len x) = n & (x * A) = y;

      

       A2: for i holds ex x be FinSequence of REAL st ( len x) = n & (x * A) = ( Base_FinSeq (n,i))

      proof

        let i;

        ( len ( Base_FinSeq (n,i))) = n by Th74;

        hence thesis by A1;

      end;

      

       A3: for j be Nat st j in ( Seg n) holds ex d be Element of ( REAL * ) st P[j, d]

      proof

        let j be Nat;

        assume j in ( Seg n);

        consider x be FinSequence of REAL such that

         A4: ( len x) = n & (x * A) = ( Base_FinSeq (n,j)) by A2;

        reconsider d0 = x as Element of ( REAL * ) by FINSEQ_1:def 11;

        for s be Nat, q be FinSequence of REAL st s = j & q = d0 holds ( len q) = n & (q * A) = ( Base_FinSeq (n,s)) by A4;

        hence thesis;

      end;

      consider f be FinSequence of ( REAL * ) such that

       A5: ( len f) = n & for j be Nat st j in ( Seg n) holds P[j, (f /. j)] from FINSEQ_4:sch 1( A3);

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

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider z be object such that

         A6: z in ( dom f) and

         A7: (f . z) = x by FUNCT_1:def 3;

        reconsider j0 = z as Nat by A6;

        reconsider q0 = (f /. j0) as FinSequence of REAL by FINSEQ_1:def 11;

        z in ( Seg ( len f)) by A6, FINSEQ_1:def 3;

        then

         A8: ( len q0) = n by A5;

        q0 = x by A6, A7, PARTFUN1:def 6;

        hence thesis by A8;

      end;

      then

      reconsider M = f as Matrix of REAL by MATRIX_0: 9;

      for p be FinSequence of REAL st p in ( rng M) holds ( len p) = n

      proof

        let p be FinSequence of REAL ;

        assume p in ( rng M);

        then

        consider z be object such that

         A9: z in ( dom f) and

         A10: (M . z) = p by FUNCT_1:def 3;

        reconsider j0 = z as Nat by A9;

        reconsider q0 = (f /. j0) as FinSequence of REAL by FINSEQ_1:def 11;

        z in ( Seg ( len f)) & q0 = p by A9, A10, FINSEQ_1:def 3, PARTFUN1:def 6;

        hence thesis by A5;

      end;

      then

      reconsider B = M as Matrix of n, REAL by A5, MATRIX_0:def 2;

      for i4,j4 be Nat st [i4, j4] in ( Indices (B * A)) holds ((B * A) * (i4,j4)) = (( 1_Rmatrix n) * (i4,j4))

      proof

        let i4,j4 be Nat;

        reconsider i = i4, j = j4 as Nat;

        consider n2 be Nat such that

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

        assume

         A12: [i4, j4] in ( Indices (B * A));

        then j in ( Seg ( width (M * A))) by ZFMISC_1: 87;

        then

         A13: 1 <= j & j <= ( width (M * A)) by FINSEQ_1: 1;

        i in ( dom (M * A)) by A12, ZFMISC_1: 87;

        then

         A14: ((M * A) . i) in ( rng (M * A)) by FUNCT_1:def 3;

        then

        consider p2 be FinSequence of REAL such that

         A15: ((M * A) . i) = p2 and

         A16: ( len p2) = n2 by A11;

        

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

        

         A18: [i, j] in [:( Seg n), ( Seg n):] by A12, MATRIX_0: 24;

        then [i, j] in ( Indices ( 1_Rmatrix n)) by MATRIX_0: 24;

        then

         A19: ex p3 be FinSequence of REAL st p3 = (( 1_Rmatrix n) . i) & (( 1_Rmatrix n) * (i,j)) = (p3 . j) by MATRIX_0:def 5;

        

         A20: ( width (B * A)) = n by MATRIX_0: 24;

        j in ( Seg n) by A18, ZFMISC_1: 87;

        then

         A21: 1 <= j & j <= n by FINSEQ_1: 1;

        

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

        then

         A23: 1 <= i & i <= n by FINSEQ_1: 1;

        

         A24: ( len (B * A)) = n & for p be FinSequence of REAL st p in ( rng (B * A)) holds ( len p) = n by MATRIX_0:def 2;

        now

          per cases ;

            case

             A25: i = j;

            reconsider g = (f /. i) as FinSequence of REAL by FINSEQ_1:def 11;

            

             A26: (g * A) = ( Base_FinSeq (n,i)) by A5, A22;

            ( len B) = n by MATRIX_0: 24;

            then (f /. i) = (M . i) by A23, FINSEQ_4: 15;

            then

             A27: g = ( Line (B,i)) by A23, A17, Lm2;

            

             A28: (( 1_Rmatrix n) * (i,j)) = (( Base_FinSeq (n,i)) . i) by A19, A23, A25, Th78

            .= 1 by A23, Th75;

            (p2 . j) = ((B * A) * (i,j)) by A24, A14, A15, A16, A13, A23, A20, Th2

            .= (( Base_FinSeq (n,i)) . j) by A12, A26, A27, Th61

            .= 1 by A23, A25, Th75;

            hence (( 1_Rmatrix n) * (i,j)) = (p2 . j) by A28;

          end;

            case

             A29: i <> j;

            reconsider g = (f /. i) as FinSequence of REAL by FINSEQ_1:def 11;

            ( len B) = n by MATRIX_0: 24;

            then (f /. i) = (M . i) by A23, FINSEQ_4: 15;

            then g = ( Line (B,i)) by A23, A17, Lm2;

            then

             A30: (( Line (B,i)) * A) = ( Base_FinSeq (n,i)) by A5, A22;

            

             A31: (( 1_Rmatrix n) * (i,j)) = (( Base_FinSeq (n,i)) . j) by A19, A23, Th78

            .= 0 by A21, A29, Th76;

            (p2 . j) = ((B * A) * (i,j)) by A24, A14, A15, A16, A13, A23, A20, Th2

            .= (( Base_FinSeq (n,i)) . j) by A12, A30, Th61

            .= 0 by A21, A29, Th76;

            hence (( 1_Rmatrix n) * (i,j)) = (p2 . j) by A31;

          end;

        end;

        hence thesis by A12, A15, MATRIX_0:def 5;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    theorem :: MATRIXR2:94

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

    proof

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

      

       A1: ( len A) = n & ( width A) = n by MATRIX_0: 24;

      assume n > 0 & ( len x) = n;

      hence thesis by A1, MATRIXR1: 52;

    end;

    theorem :: MATRIXR2:95

    

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

    proof

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

      

       A1: ( len A) = n & ( width A) = n by MATRIX_0: 24;

      assume n > 0 & ( len x) = n;

      hence thesis by A1, MATRIXR1: 53;

    end;

    theorem :: MATRIXR2:96

    

     Th96: for A be Matrix of n, REAL st n > 0 & (for y be FinSequence of REAL st ( len y) = n holds (ex x be FinSequence of REAL st ( len x) = n & (A * x) = y)) holds ex B be Matrix of n, REAL st (A * B) = ( 1_Rmatrix n)

    proof

      let A be Matrix of n, REAL ;

      assume that

       A1: n > 0 and

       A2: for y be FinSequence of REAL st ( len y) = n holds ex x be FinSequence of REAL st ( len x) = n & (A * x) = y;

      for y be FinSequence of REAL st ( len y) = n holds ex x be FinSequence of REAL st ( len x) = n & (x * (A @ )) = y

      proof

        let y be FinSequence of REAL ;

        assume ( len y) = n;

        then

        consider x0 be FinSequence of REAL such that

         A3: ( len x0) = n and

         A4: (A * x0) = y by A2;

        (x0 * (A @ )) = (A * x0) by A1, A3, Th95;

        hence thesis by A3, A4;

      end;

      then

      consider B be Matrix of n, REAL such that

       A5: (B * (A @ )) = ( 1_Rmatrix n) by Th93;

      ((B * (A @ )) @ ) = ( 1_Rmatrix n) by A5, Th64;

      then (((A @ ) @ ) * (B @ )) = ( 1_Rmatrix n) by Th30;

      then (A * (B @ )) = ( 1_Rmatrix n) by Th29;

      hence thesis;

    end;

    theorem :: MATRIXR2:97

    for A be Matrix of n, REAL st n > 0 & (for y be FinSequence of REAL st ( len y) = n holds (ex x1,x2 be FinSequence of REAL st ( len x1) = n & ( len x2) = n & (A * x1) = y & (x2 * A) = y)) holds A is invertible

    proof

      let A be Matrix of n, REAL ;

      assume that

       A1: n > 0 and

       A2: for y be FinSequence of REAL st ( len y) = n holds ex x1,x2 be FinSequence of REAL st ( len x1) = n & ( len x2) = n & (A * x1) = y & (x2 * A) = y;

      for y be FinSequence of REAL st ( len y) = n holds ex x be FinSequence of REAL st ( len x) = n & (x * A) = y

      proof

        let y be FinSequence of REAL ;

        assume ( len y) = n;

        then ex x1,x2 be FinSequence of REAL st ( len x1) = n & ( len x2) = n & (A * x1) = y & (x2 * A) = y by A2;

        hence thesis;

      end;

      then

       A3: ex B1 be Matrix of n, REAL st (B1 * A) = ( 1_Rmatrix n) by Th93;

      for y be FinSequence of REAL st ( len y) = n holds ex x be FinSequence of REAL st ( len x) = n & (A * x) = y

      proof

        let y be FinSequence of REAL ;

        assume ( len y) = n;

        then ex x1,x2 be FinSequence of REAL st ( len x1) = n & ( len x2) = n & (A * x1) = y & (x2 * A) = y by A2;

        hence thesis;

      end;

      then ex B2 be Matrix of n, REAL st (A * B2) = ( 1_Rmatrix n) by A1, Th96;

      hence thesis by A3, Th80;

    end;