:: MATRIXR1 semantic presentation

begin


theorem :: MATRIXR1:1
for r1, r2 being Real
for fr1, fr2 being Element of F_Real st r1 = fr1 & r2 = fr2 holds
r1 + r2 = fr1 + fr2 ;

theorem :: MATRIXR1:2
for r1, r2 being Real
for fr1, fr2 being Element of F_Real st r1 = fr1 & r2 = fr2 holds
r1 * r2 = fr1 * fr2 ;

theorem Th3: :: MATRIXR1:3
for F being FinSequence of REAL holds
( F + (- F) = 0* (len F) & F - F = 0* (len F) )
proof
let F be FinSequence of REAL ; ::_thesis: ( F + (- F) = 0* (len F) & F - F = 0* (len F) )
set n = len F;
reconsider R = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
A1: R + (- R) = (len F) |-> 0 by RVSUM_1:22;
hence  F + (- F) = 0* (len F) by EUCLID:def_4; ::_thesis: F - F = 0* (len F)
thus  F - F = 0* (len F) by A1, EUCLID:def_4; ::_thesis: verum
end;

theorem :: MATRIXR1:4
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 - F2 = F1 + (- F2) ;

theorem :: MATRIXR1:5
for F being FinSequence of REAL holds F - (0* (len F)) = F
proof
let F be FinSequence of REAL ; ::_thesis: F - (0* (len F)) = F
set n = len F;
reconsider R = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
 R - ((len F) |-> 0) = R by RVSUM_1:32;
hence  F - (0* (len F)) = F by EUCLID:def_4; ::_thesis: verum
end;

theorem :: MATRIXR1:6
for F being FinSequence of REAL holds (0* (len F)) - F = - F
proof
let F be FinSequence of REAL ; ::_thesis: (0* (len F)) - F = - F
set n = len F;
reconsider R = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
 ((len F) |-> 0) - R = - R by RVSUM_1:33;
hence  (0* (len F)) - F = - F by EUCLID:def_4; ::_thesis: verum
end;

theorem :: MATRIXR1:7
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 - (- F2) = F1 + F2 ;

theorem :: MATRIXR1:8
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
- (F1 - F2) = F2 - F1 by RVSUM_1:35;

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

theorem :: MATRIXR1:10
for F1, F2 being FinSequence of REAL st len F1 = len F2 & F1 - F2 = 0* (len F1) holds
F1 = F2
proof
let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 & F1 - F2 = 0* (len F1) implies F1 = F2 )
set n = len F1;
assume  len F1 = len F2 ; ::_thesis: ( not F1 - F2 = 0* (len F1) or F1 = F2 )
then reconsider R1 = F1, R2 = F2 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92;
 ( R1 - R2 = (len F1) |-> 0 implies R1 = R2 ) by RVSUM_1:38;
hence  ( not F1 - F2 = 0* (len F1) or F1 = F2 ) by EUCLID:def_4; ::_thesis: verum
end;

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

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

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

theorem Th14: :: MATRIXR1:14
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 = (F1 + F2) - F2
proof
let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 implies F1 = (F1 + F2) - F2 )
set n = len F1;
assume  len F1 = len F2 ; ::_thesis: F1 = (F1 + F2) - F2
then reconsider R1 = F1, R2 = F2 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92;
 R1 = (R1 + R2) - R2 by RVSUM_1:42;
hence  F1 = (F1 + F2) - F2 ; ::_thesis: verum
end;

theorem :: MATRIXR1:15
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 = (F1 - F2) + F2
proof
let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 implies F1 = (F1 - F2) + F2 )
set n = len F1;
assume  len F1 = len F2 ; ::_thesis: F1 = (F1 - F2) + F2
then reconsider R1 = F1, R2 = F2 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92;
 R1 = (R1 - R2) + R2 by RVSUM_1:43;
hence  F1 = (F1 - F2) + F2 ; ::_thesis: verum
end;

begin

theorem Th16: :: MATRIXR1:16
for K being non empty multMagma
for p being FinSequence of K
for a being Element of K holds len (a * p) = len p
proof
let K be non empty multMagma ; ::_thesis: for p being FinSequence of K
for a being Element of K holds len (a * p) = len p
let p be FinSequence of K; ::_thesis: for a being Element of K holds len (a * p) = len p
let a be Element of K; ::_thesis: len (a * p) = len p
reconsider q = p as Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
 a * q in (len p) -tuples_on the carrier of K ;
then  a * q in  {  s where s is Element of the carrier of K * : len s = len p  }  by FINSEQ_2:def_4;
then  ex s being Element of the carrier of K * st
( a * q = s & len s = len p ) ;
hence  len (a * p) = len p ; ::_thesis: verum
end;

theorem Th17: :: MATRIXR1:17
for r being Real
for fr being Element of F_Real
for p being FinSequence of REAL
for fp being FinSequence of F_Real st r = fr & p = fp holds
r * p = fr * fp
proof
let r be Real; ::_thesis: for fr being Element of F_Real
for p being FinSequence of REAL
for fp being FinSequence of F_Real st r = fr & p = fp holds
r * p = fr * fp
let fr be Element of F_Real; ::_thesis: for p being FinSequence of REAL
for fp being FinSequence of F_Real st r = fr & p = fp holds
r * p = fr * fp
let p be FinSequence of REAL ; ::_thesis: for fp being FinSequence of F_Real st r = fr & p = fp holds
r * p = fr * fp
let fp be FinSequence of F_Real; ::_thesis: ( r = fr & p = fp implies r * p = fr * fp )
assume that
A1: r = fr and
A2: p = fp ; ::_thesis: r * p = fr * fp
A3: len (r * p) = len fp by A2, RVSUM_1:117;
then A4: len (r * p) = len (fr * fp) by Th16;
 for i being Nat st 1 <= i & i <= len (r * p) holds
(r * p) . i = (fr * fp) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (r * p) implies (r * p) . i = (fr * fp) . i )
assume  ( 1 <= i & i <= len (r * p) ) ; ::_thesis: (r * p) . i = (fr * fp) . i
then  i in Seg (len fp) by A3, FINSEQ_1:1;
then A5: i in dom (fr * fp) by A3, A4, FINSEQ_1:def_3;
reconsider s = fp . i as Element of F_Real ;
thus (r * p) . i = fr * s by A1, A2, RVSUM_1:44
.= (fr * fp) . i by A5, FVSUM_1:50 ; ::_thesis: verum
end;
hence  r * p = fr * fp by A4, FINSEQ_1:14; ::_thesis: verum
end;

theorem :: MATRIXR1:18
for K being Field
for a being Element of K
for A being Matrix of K holds Indices (a * A) = Indices A
proof
let K be Field; ::_thesis: for a being Element of K
for A being Matrix of K holds Indices (a * A) = Indices A
let a be Element of K; ::_thesis: for A being Matrix of K holds Indices (a * A) = Indices A
let A be Matrix of K; ::_thesis: Indices (a * A) = Indices A
 ( len (a * A) = len A & width (a * A) = width A ) by MATRIX_3:def_5;
hence  Indices (a * A) = Indices A by FINSEQ_3:29; ::_thesis: verum
end;

theorem Th19: :: MATRIXR1:19
for i being Nat
for K being Field
for a being Element of K
for M being Matrix of K st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
proof
let i be Nat; ::_thesis: for K being Field
for a being Element of K
for M being Matrix of K st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
let K be Field; ::_thesis: for a being Element of K
for M being Matrix of K st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
let a be Element of K; ::_thesis: for M being Matrix of K st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
let M be Matrix of K; ::_thesis: ( 1 <= i & i <= width M implies Col ((a * M),i) = a * (Col (M,i)) )
assume A1: ( 1 <= i & i <= width M ) ; ::_thesis: Col ((a * M),i) = a * (Col (M,i))
A2: Seg (len (a * M)) = dom (a * M) by FINSEQ_1:def_3;
A3: len (a * M) = len M by MATRIX_3:def_5;
then A4: dom M = dom (a * M) by FINSEQ_3:29;
A5: ( len (a * (Col (M,i))) = len (Col (M,i)) & len (Col (M,i)) = len M ) by Th16, MATRIX_1:def_8;
then A6: dom (a * (Col (M,i))) = Seg (len (a * M)) by A3, FINSEQ_1:def_3;
 for j being Nat st j in dom (a * M) holds
(a * (Col (M,i))) . j = (a * M) * (j,i)
proof
let j be Nat; ::_thesis: ( j in dom (a * M) implies (a * (Col (M,i))) . j = (a * M) * (j,i) )
assume A7: j in dom (a * M) ; ::_thesis: (a * (Col (M,i))) . j = (a * M) * (j,i)
 i in Seg (width M) by A1, FINSEQ_1:1;
then  [j,i] in Indices M by A4, A7, ZFMISC_1:87;
then A8: (a * M) * (j,i) = a * (M * (j,i)) by MATRIX_3:def_5;
 (Col (M,i)) . j = M * (j,i) by A4, A7, MATRIX_1:def_8;
hence  (a * (Col (M,i))) . j = (a * M) * (j,i) by A6, A2, A7, A8, FVSUM_1:50; ::_thesis: verum
end;
hence  Col ((a * M),i) = a * (Col (M,i)) by A5, A3, MATRIX_1:def_8; ::_thesis: verum
end;

theorem :: MATRIXR1:20
for K being Field
for a being Element of K
for M being Matrix of K
for i being Nat st 1 <= i & i <= len M holds
Line ((a * M),i) = a * (Line (M,i))
proof
let K be Field; ::_thesis: for a being Element of K
for M being Matrix of K
for i being Nat st 1 <= i & i <= len M holds
Line ((a * M),i) = a * (Line (M,i))
let a be Element of K; ::_thesis: for M being Matrix of K
for i being Nat st 1 <= i & i <= len M holds
Line ((a * M),i) = a * (Line (M,i))
let M be Matrix of K; ::_thesis: for i being Nat st 1 <= i & i <= len M holds
Line ((a * M),i) = a * (Line (M,i))
let i be Nat; ::_thesis: ( 1 <= i & i <= len M implies Line ((a * M),i) = a * (Line (M,i)) )
assume A1: ( 1 <= i & i <= len M ) ; ::_thesis: Line ((a * M),i) = a * (Line (M,i))
A2: width (a * M) = width M by MATRIX_3:def_5;
A3: Seg (width M) = Seg (width (a * M)) by MATRIX_3:def_5;
A4: ( len (a * (Line (M,i))) = len (Line (M,i)) & len (Line (M,i)) = width M ) by Th16, MATRIX_1:def_7;
then A5: dom (a * (Line (M,i))) = Seg (width (a * M)) by A2, FINSEQ_1:def_3;
 for j being Nat st j in Seg (width (a * M)) holds
(a * (Line (M,i))) . j = (a * M) * (i,j)
proof
let j be Nat; ::_thesis: ( j in Seg (width (a * M)) implies (a * (Line (M,i))) . j = (a * M) * (i,j) )
assume A6: j in Seg (width (a * M)) ; ::_thesis: (a * (Line (M,i))) . j = (a * M) * (i,j)
 i in dom M by A1, FINSEQ_3:25;
then  [i,j] in Indices M by A3, A6, ZFMISC_1:87;
then A7: (a * M) * (i,j) = a * (M * (i,j)) by MATRIX_3:def_5;
 (Line (M,i)) . j = M * (i,j) by A3, A6, MATRIX_1:def_7;
hence  (a * (Line (M,i))) . j = (a * M) * (i,j) by A5, A6, A7, FVSUM_1:50; ::_thesis: verum
end;
hence  Line ((a * M),i) = a * (Line (M,i)) by A4, A2, MATRIX_1:def_7; ::_thesis: verum
end;

theorem :: MATRIXR1:21
for K being Field
for A, B being Matrix of K st width A = len B holds
ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )
proof
let K be Field; ::_thesis: for A, B being Matrix of K st width A = len B holds
ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )
let A, B be Matrix of K; ::_thesis: ( width A = len B implies ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) )
assume A1: width A = len B ; ::_thesis: ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )
deffunc H1( Nat, Nat) ->  Element of the carrier of K = (Line (A,$1)) "*" (Col (B,$2));
consider M being Matrix of len A, width B, the carrier of K such that
A2: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H1(i,j) from MATRIX_1:sch_1();
percases ( len A > 0 or len A = 0 ) ;
suppose len A > 0 ; ::_thesis: ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )
then  ( len M = len A & width M = width B ) by MATRIX_1:23;
hence  ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) by A2; ::_thesis: verum
end;
supposeA3: len A = 0 ; ::_thesis: ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )
then A4: len M = 0 by MATRIX_1:25;
 len B = 0 by A1, A3, MATRIX_1:def_3;
then  width B = 0 by MATRIX_1:def_3;
then  width M = width B by A4, MATRIX_1:def_3;
hence  ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) by A2, A3, A4; ::_thesis: verum
end;
end;
end;

theorem Th22: :: MATRIXR1:22
for K being Field
for a being Element of K
for A, B being Matrix of K st width A = len B holds
A * (a * B) = a * (A * B)
proof
let K be Field; ::_thesis: for a being Element of K
for A, B being Matrix of K st width A = len B holds
A * (a * B) = a * (A * B)
let a be Element of K; ::_thesis: for A, B being Matrix of K st width A = len B holds
A * (a * B) = a * (A * B)
let A, B be Matrix of K; ::_thesis: ( width A = len B implies A * (a * B) = a * (A * B) )
set C = a * B;
set D = a * (A * B);
A1: len (a * (A * B)) = len (A * B) by MATRIX_3:def_5;
assume A2: width A = len B ; ::_thesis: A * (a * B) = a * (A * B)
then  width (A * B) = width B by MATRIX_3:def_4;
then A3: width (a * (A * B)) = width B by MATRIX_3:def_5
.= width (a * B) by MATRIX_3:def_5 ;
A4: width B = width (a * B) by MATRIX_3:def_5;
A5: for i, j being Nat st [i,j] in Indices (a * (A * B)) holds
(a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * (A * B)) implies (a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j)) )
reconsider xo = Col (B,j) as Element of (width A) -tuples_on the carrier of K by A2;
assume A6: [i,j] in Indices (a * (A * B)) ; ::_thesis: (a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j))
then  j in Seg (width B) by A4, A3, ZFMISC_1:87;
then A7: ( 1 <= j & j <= width B ) by FINSEQ_1:1;
 dom (A * B) = dom (a * (A * B)) by A1, FINSEQ_3:29;
then A8: [i,j] in Indices (A * B) by A6, MATRIX_3:def_5;
then  (a * (A * B)) * (i,j) = a * ((A * B) * (i,j)) by MATRIX_3:def_5;
then (a * (A * B)) * (i,j) = a * ((Line (A,i)) "*" (Col (B,j))) by A2, A8, MATRIX_3:def_4
.= a * (Sum (mlt ((Line (A,i)),(Col (B,j))))) by FVSUM_1:def_9
.= Sum (a * (mlt ((Line (A,i)),(Col (B,j))))) by FVSUM_1:73
.= Sum (mlt ((Line (A,i)),(a * xo))) by FVSUM_1:69
.= Sum (mlt ((Line (A,i)),(Col ((a * B),j)))) by A7, Th19 ;
hence  (a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j)) by FVSUM_1:def_9; ::_thesis: verum
end;
 ( len (a * B) = len B & len (A * B) = len A ) by A2, MATRIX_3:def_4, MATRIX_3:def_5;
hence  A * (a * B) = a * (A * B) by A2, A1, A3, A5, MATRIX_3:def_4; ::_thesis: verum
end;

definition
let A be Matrix of REAL;
func MXR2MXF A ->  Matrix of F_Real equals :: MATRIXR1:def 1
A;
coherence
 A is Matrix of F_Real ;
end;

:: deftheorem  defines MXR2MXF MATRIXR1:def_1_:_
 for A being Matrix of REAL holds MXR2MXF A = A;

definition
let A be Matrix of F_Real;
func MXF2MXR A ->  Matrix of REAL equals :: MATRIXR1:def 2
A;
coherence
 A is Matrix of REAL ;
end;

:: deftheorem  defines MXF2MXR MATRIXR1:def_2_:_
 for A being Matrix of F_Real holds MXF2MXR A = A;

theorem :: MATRIXR1:23
for D1, D2 being set
for A being Matrix of D1
for B being Matrix of D2 st A = B holds
for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)
proof
let D1, D2 be set ; ::_thesis: for A being Matrix of D1
for B being Matrix of D2 st A = B holds
for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)
let A be Matrix of D1; ::_thesis: for B being Matrix of D2 st A = B holds
for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)
let B be Matrix of D2; ::_thesis: ( A = B implies for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j) )
assume A1: A = B ; ::_thesis: for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies A * (i,j) = B * (i,j) )
assume A2: [i,j] in Indices A ; ::_thesis: A * (i,j) = B * (i,j)
then A3: ex p being FinSequence of D1 st
( p = A . i & A * (i,j) = p . j ) by MATRIX_1:def_5;
 ex q being FinSequence of D2 st
( q = B . i & B * (i,j) = q . j ) by A1, A2, MATRIX_1:def_5;
hence  A * (i,j) = B * (i,j) by A1, A3; ::_thesis: verum
end;

theorem :: MATRIXR1:24
for K being Field
for A, B being Matrix of K holds Indices (A + B) = Indices A
proof
let K be Field; ::_thesis: for A, B being Matrix of K holds Indices (A + B) = Indices A
let A, B be Matrix of K; ::_thesis: Indices (A + B) = Indices A
 ( len (A + B) = len A & width (A + B) = width A ) by MATRIX_3:def_3;
hence  Indices (A + B) = Indices A by MATRIX_4:55; ::_thesis: verum
end;

definition
let A, B be Matrix of REAL;
funcA + B ->  Matrix of REAL equals :: MATRIXR1:def 3
 MXF2MXR ((MXR2MXF A) + (MXR2MXF B));
coherence
 MXF2MXR ((MXR2MXF A) + (MXR2MXF B)) is Matrix of REAL ;
end;

:: deftheorem  defines + MATRIXR1:def_3_:_
 for A, B being Matrix of REAL holds A + B = MXF2MXR ((MXR2MXF A) + (MXR2MXF B));

theorem Th25: :: MATRIXR1:25
for A, B being Matrix of REAL holds
( len (A + B) = len A & width (A + B) = width A & ( for i, j being Nat st [i,j] in Indices A holds
(A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) ) )
proof
let A, B be Matrix of REAL; ::_thesis: ( len (A + B) = len A & width (A + B) = width A & ( for i, j being Nat st [i,j] in Indices A holds
(A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) ) )
thus  ( len (A + B) = len A & width (A + B) = width A ) by MATRIX_3:def_3; ::_thesis: for i, j being Nat st [i,j] in Indices A holds
(A + B) * (i,j) = (A * (i,j)) + (B * (i,j))
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies (A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) )
assume  [i,j] in Indices A ; ::_thesis: (A + B) * (i,j) = (A * (i,j)) + (B * (i,j))
then  (A + B) * (i,j) = ((MXR2MXF A) * (i,j)) + ((MXR2MXF B) * (i,j)) by MATRIX_3:def_3;
hence  (A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) ; ::_thesis: verum
end;

theorem Th26: :: MATRIXR1:26
for A, B, C being Matrix of REAL st len C = len A & width C = width A & ( for i, j being 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; ::_thesis: ( len C = len A & width C = width A & ( for i, j being Nat st [i,j] in Indices A holds
C * (i,j) = (A * (i,j)) + (B * (i,j)) ) implies C = A + B )
assume that
A1: ( len C = len A & width C = width A ) and
A2: for i, j being Nat st [i,j] in Indices A holds
C * (i,j) = (A * (i,j)) + (B * (i,j)) ; ::_thesis: C = A + B
set B2 = MXR2MXF B;
set A2 = MXR2MXF A;
set D = MXR2MXF C;
 for i, j being Nat st [i,j] in Indices (MXR2MXF A) holds
(MXR2MXF C) * (i,j) = ((MXR2MXF A) * (i,j)) + ((MXR2MXF B) * (i,j)) by A2;
hence  C = A + B by A1, MATRIX_3:def_3; ::_thesis: verum
end;

definition
let A be Matrix of REAL;
func - A ->  Matrix of REAL equals :: MATRIXR1:def 4
 MXF2MXR (- (MXR2MXF A));
coherence
 MXF2MXR (- (MXR2MXF A)) is Matrix of REAL ;
end;

:: deftheorem  defines - MATRIXR1:def_4_:_
 for A being Matrix of REAL holds - A = MXF2MXR (- (MXR2MXF A));

definition
let A, B be Matrix of REAL;
funcA - B ->  Matrix of REAL equals :: MATRIXR1:def 5
 MXF2MXR ((MXR2MXF A) - (MXR2MXF B));
coherence
 MXF2MXR ((MXR2MXF A) - (MXR2MXF B)) is Matrix of REAL ;
funcA * B ->  Matrix of REAL equals :: MATRIXR1:def 6
 MXF2MXR ((MXR2MXF A) * (MXR2MXF B));
coherence
 MXF2MXR ((MXR2MXF A) * (MXR2MXF B)) is Matrix of REAL ;
end;

:: deftheorem  defines - MATRIXR1:def_5_:_
 for A, B being Matrix of REAL holds A - B = MXF2MXR ((MXR2MXF A) - (MXR2MXF B));

:: deftheorem  defines * MATRIXR1:def_6_:_
 for A, B being Matrix of REAL holds A * B = MXF2MXR ((MXR2MXF A) * (MXR2MXF B));

definition
let a be real number ;
let A be Matrix of REAL;
funca * A ->  Matrix of REAL means :Def7: :: MATRIXR1:def 7
 for ea being Element of F_Real st ea = a holds
it = MXF2MXR (ea * (MXR2MXF A));
existence
 ex b1 being Matrix of REAL st
for ea being Element of F_Real st ea = a holds
b1 = MXF2MXR (ea * (MXR2MXF A))
proof
reconsider aa = a as Element of F_Real by XREAL_0:def_1;
set C = MXF2MXR (aa * (MXR2MXF A));
 for ea being Element of F_Real st ea = a holds
MXF2MXR (aa * (MXR2MXF A)) = MXF2MXR (ea * (MXR2MXF A)) ;
hence  ex b1 being Matrix of REAL st
for ea being Element of F_Real st ea = a holds
b1 = MXF2MXR (ea * (MXR2MXF A)) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Matrix of REAL st ( for ea being Element of F_Real st ea = a holds
b1 = MXF2MXR (ea * (MXR2MXF A)) ) & ( for ea being Element of F_Real st ea = a holds
b2 = MXF2MXR (ea * (MXR2MXF A)) ) holds
b1 = b2
proof
reconsider aa = a as Element of F_Real by XREAL_0:def_1;
let C1, C2 be Matrix of REAL; ::_thesis: ( ( for ea being Element of F_Real st ea = a holds
C1 = MXF2MXR (ea * (MXR2MXF A)) ) & ( for ea being Element of F_Real st ea = a holds
C2 = MXF2MXR (ea * (MXR2MXF A)) ) implies C1 = C2 )
assume that
A1: for ea being Element of F_Real st ea = a holds
C1 = MXF2MXR (ea * (MXR2MXF A)) and
A2: for ea being Element of F_Real st ea = a holds
C2 = MXF2MXR (ea * (MXR2MXF A)) ; ::_thesis: C1 = C2
 C2 = MXF2MXR (aa * (MXR2MXF A)) by A2;
hence  C1 = C2 by A1; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines * MATRIXR1:def_7_:_
 for a being real number
for A, b3 being Matrix of REAL holds
( b3 = a * A iff for ea being Element of F_Real st ea = a holds
b3 = MXF2MXR (ea * (MXR2MXF A)) );

theorem Th27: :: MATRIXR1:27
for a being Real
for A being Matrix of REAL holds
( len (a * A) = len A & width (a * A) = width A )
proof
let a be Real; ::_thesis: for A being Matrix of REAL holds
( len (a * A) = len A & width (a * A) = width A )
let A be Matrix of REAL; ::_thesis: ( len (a * A) = len A & width (a * A) = width A )
reconsider ea = a as Element of F_Real ;
thus  len (a * A) = len (MXF2MXR (ea * (MXR2MXF A))) by Def7
.= len A by MATRIX_3:def_5 ; ::_thesis: width (a * A) = width A
thus  width (a * A) = width (MXF2MXR (ea * (MXR2MXF A))) by Def7
.= width A by MATRIX_3:def_5 ; ::_thesis: verum
end;

theorem Th28: :: MATRIXR1:28
for a being Real
for A being Matrix of REAL holds Indices (a * A) = Indices A
proof
let a be Real; ::_thesis: for A being Matrix of REAL holds Indices (a * A) = Indices A
let A be Matrix of REAL; ::_thesis: Indices (a * A) = Indices A
 ( len A = len (a * A) & width (a * A) = width A ) by Th27;
hence  Indices (a * A) = Indices A by MATRIX_4:55; ::_thesis: verum
end;

theorem Th29: :: MATRIXR1:29
for a being Real
for A being Matrix of REAL
for i2, j2 being Nat st [i2,j2] in Indices A holds
(a * A) * (i2,j2) = a * (A * (i2,j2))
proof
let a be Real; ::_thesis: for A being Matrix of REAL
for i2, j2 being Nat st [i2,j2] in Indices A holds
(a * A) * (i2,j2) = a * (A * (i2,j2))
let A be Matrix of REAL; ::_thesis: for i2, j2 being Nat st [i2,j2] in Indices A holds
(a * A) * (i2,j2) = a * (A * (i2,j2))
let i2, j2 be Nat; ::_thesis: ( [i2,j2] in Indices A implies (a * A) * (i2,j2) = a * (A * (i2,j2)) )
reconsider ea = a as Element of F_Real ;
assume  [i2,j2] in Indices A ; ::_thesis: (a * A) * (i2,j2) = a * (A * (i2,j2))
then (MXF2MXR (ea * (MXR2MXF A))) * (i2,j2) = ea * ((MXR2MXF A) * (i2,j2)) by MATRIX_3:def_5
.= a * (A * (i2,j2)) ;
hence  (a * A) * (i2,j2) = a * (A * (i2,j2)) by Def7; ::_thesis: verum
end;

theorem Th30: :: MATRIXR1:30
for a being Real
for A being Matrix of REAL st width A > 0 holds
(a * A) @ = a * (A @)
proof
let a be Real; ::_thesis: for A being Matrix of REAL st width A > 0 holds
(a * A) @ = a * (A @)
let A be Matrix of REAL; ::_thesis: ( width A > 0 implies (a * A) @ = a * (A @) )
assume  width A > 0 ; ::_thesis: (a * A) @ = a * (A @)
then A1: len (A @) = width A by MATRIX_2:10;
A2: for i, j being Nat holds
( [i,j] in Indices (a * (A @)) iff [j,i] in Indices (a * A) )
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * (A @)) iff [j,i] in Indices (a * A) )
 ( Indices (a * (A @)) = Indices (A @) & Indices (a * A) = Indices A ) by Th28;
hence  ( [i,j] in Indices (a * (A @)) iff [j,i] in Indices (a * A) ) by MATRIX_1:def_6; ::_thesis: verum
end;
A3: for i, j being Nat st [j,i] in Indices (a * A) holds
(a * (A @)) * (i,j) = (a * A) * (j,i)
proof
let i, j be Nat; ::_thesis: ( [j,i] in Indices (a * A) implies (a * (A @)) * (i,j) = (a * A) * (j,i) )
assume  [j,i] in Indices (a * A) ; ::_thesis: (a * (A @)) * (i,j) = (a * A) * (j,i)
then A4: [j,i] in Indices A by Th28;
then  [i,j] in Indices (A @) by MATRIX_1:def_6;
then  (a * (A @)) * (i,j) = a * ((A @) * (i,j)) by Th29;
then (a * (A @)) * (i,j) = a * (A * (j,i)) by A4, MATRIX_1:def_6
.= (a * A) * (j,i) by A4, Th29 ;
hence  (a * (A @)) * (i,j) = (a * A) * (j,i) ; ::_thesis: verum
end;
 ( len (a * (A @)) = len (A @) & width A = width (a * A) ) by Th27;
hence  (a * A) @ = a * (A @) by A1, A2, A3, MATRIX_1:def_6; ::_thesis: verum
end;

theorem :: MATRIXR1:31
for a being Real
for i being Nat
for A being Matrix of REAL st len A > 0 & i in dom A holds
( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q ) )
proof
let a be Real; ::_thesis: for i being Nat
for A being Matrix of REAL st len A > 0 & i in dom A holds
( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q ) )
let i be Nat; ::_thesis: for A being Matrix of REAL st len A > 0 & i in dom A holds
( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q ) )
let A be Matrix of REAL; ::_thesis: ( len A > 0 & i in dom A implies ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q ) ) )
assume that
A1: len A > 0 and
A2: i in dom A ; ::_thesis: ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q ) )
consider n3 being Nat such that
A3: for x being set st x in rng A holds
ex s2 being FinSequence st
( s2 = x & len s2 = n3 ) by MATRIX_1:def_1;
 A . i in rng A by A2, FUNCT_1:def_3;
then A4: ex qq0 being FinSequence st
( qq0 = A . i & len qq0 = n3 ) by A3;
 len (a * A) = len A by Th27;
then consider s being FinSequence such that
A5: s in rng (a * A) and
A6: len s = width (a * A) by A1, MATRIX_1:def_3;
A7: width (a * A) = width A by Th27;
consider s3 being FinSequence such that
A8: s3 in rng A and
A9: len s3 = width A by A1, MATRIX_1:def_3;
consider n2 being Nat such that
A10: for x being set st x in rng (a * A) holds
ex s2 being FinSequence st
( s2 = x & len s2 = n2 ) by MATRIX_1:def_1;
 len (a * A) = len A by Th27;
then A11: dom (a * A) = dom A by FINSEQ_3:29;
then  (a * A) . i in rng (a * A) by A2, FUNCT_1:def_3;
then consider qq being FinSequence such that
A12: qq = (a * A) . i and
A13: len qq = n2 by A10;
consider n being Nat such that
A14: for x being set st x in rng A holds
ex p being FinSequence of REAL st
( x = p & len p = n ) by MATRIX_1:9;
 A . i in rng A by A2, FUNCT_1:def_3;
then  ex p2 being FinSequence of REAL st
( A . i = p2 & len p2 = n ) by A14;
hence  ex p being FinSequence of REAL st p = A . i ; ::_thesis: for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q
let q be FinSequence of REAL ; ::_thesis: ( q = A . i implies (a * A) . i = a * q )
assume A15: q = A . i ; ::_thesis: (a * A) . i = a * q
A16: ex s4 being FinSequence st
( s4 = s3 & len s4 = n3 ) by A8, A3;
then A17: len (a * q) = width A by A15, A9, A4, RVSUM_1:117;
A18: for j being Nat st 1 <= j & j <= len (a * q) holds
qq . j = (a * q) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= len (a * q) implies qq . j = (a * q) . j )
assume  ( 1 <= j & j <= len (a * q) ) ; ::_thesis: qq . j = (a * q) . j
then A19: j in Seg (width A) by A17, FINSEQ_1:1;
then A20: [i,j] in Indices A by A2, ZFMISC_1:87;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
 [i,j] in Indices (a * A) by A2, A7, A11, A19, ZFMISC_1:87;
then A21: ex p being FinSequence of REAL st
( p = (a * A) . i & (a * A) * (i,j) = p . j ) by MATRIX_1:def_5;
 ex p2 being FinSequence of REAL st
( p2 = A . i & A * (i,j) = p2 . j ) by A20, MATRIX_1:def_5;
then  qq . j = a * (q . j) by A15, A12, A20, A21, Th29;
hence  qq . j = (a * q) . j by RVSUM_1:44; ::_thesis: verum
end;
 ex s2 being FinSequence st
( s2 = s & len s2 = n2 ) by A5, A10;
then  width A = len qq by A6, A13, Th27;
hence  (a * A) . i = a * q by A15, A9, A16, A12, A4, A18, FINSEQ_1:14, RVSUM_1:117; ::_thesis: verum
end;

theorem :: MATRIXR1:32
for A being Matrix of REAL holds 1 * A = A
proof
let A be Matrix of REAL; ::_thesis: 1 * A = A
 1 * A = MXF2MXR ((1_ F_Real) * (MXR2MXF A)) by Def7;
hence  1 * A = A by MATRIX_5:9; ::_thesis: verum
end;

theorem :: MATRIXR1:33
for A being Matrix of REAL holds A + A = 2 * A
proof
set e2 = (1_ F_Real) + (1_ F_Real);
let A be Matrix of REAL; ::_thesis: A + A = 2 * A
A1: (1_ F_Real) * (MXR2MXF A) = MXR2MXF A by MATRIX_5:9;
2 * A = MXF2MXR (((1_ F_Real) + (1_ F_Real)) * (MXR2MXF A)) by Def7
.= MXF2MXR ((MXR2MXF A) + (MXR2MXF A)) by A1, MATRIX_5:12 ;
hence  A + A = 2 * A ; ::_thesis: verum
end;

theorem :: MATRIXR1:34
for A being Matrix of REAL holds (A + A) + A = 3 * A
proof
reconsider e3 = ((1_ F_Real) + (1_ F_Real)) + (1_ F_Real) as Element of F_Real ;
let A be Matrix of REAL; ::_thesis: (A + A) + A = 3 * A
A1: ( len A = len (MXR2MXF A) & width A = width (MXR2MXF A) ) ;
3 * A = MXF2MXR (e3 * (MXR2MXF A)) by Def7
.= MXF2MXR (((1_ F_Real) * (MXR2MXF A)) + (((1_ F_Real) + (1_ F_Real)) * (MXR2MXF A))) by MATRIX_5:12
.= MXF2MXR ((MXR2MXF A) + (((1_ F_Real) + (1_ F_Real)) * (MXR2MXF A))) by MATRIX_5:9
.= MXF2MXR ((MXR2MXF A) + (((1_ F_Real) * (MXR2MXF A)) + ((1_ F_Real) * (MXR2MXF A)))) by MATRIX_5:12
.= MXF2MXR ((MXR2MXF A) + ((MXR2MXF A) + ((1_ F_Real) * (MXR2MXF A)))) by MATRIX_5:9
.= MXF2MXR ((MXR2MXF A) + ((MXR2MXF A) + (MXR2MXF A))) by MATRIX_5:9
.= MXF2MXR (((MXR2MXF A) + (MXR2MXF A)) + (MXR2MXF A)) by A1, MATRIX_3:3 ;
hence  (A + A) + A = 3 * A ; ::_thesis: verum
end;

definition
let n, m be Nat;
func 0_Rmatrix (n,m) ->  Matrix of REAL equals :: MATRIXR1:def 8
 MXF2MXR (0. (F_Real,n,m));
coherence
 MXF2MXR (0. (F_Real,n,m)) is Matrix of REAL ;
end;

:: deftheorem  defines 0_Rmatrix MATRIXR1:def_8_:_
 for n, m being Nat holds 0_Rmatrix (n,m) = MXF2MXR (0. (F_Real,n,m));

theorem :: MATRIXR1:35
for A, B being Matrix of REAL holds A - (- B) = A + B
proof
let A, B be Matrix of REAL; ::_thesis: A - (- B) = A + B
 A + B = MXF2MXR ((MXR2MXF A) + (MXR2MXF (- (- B)))) by MATRIX_4:1;
hence  A - (- B) = A + B by MATRIX_4:def_1; ::_thesis: verum
end;

theorem Th36: :: MATRIXR1:36
for n, m being Nat
for A being Matrix of REAL st len A = n & width A = m & n > 0 holds
( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A )
proof
let n, m be Nat; ::_thesis: for A being Matrix of REAL st len A = n & width A = m & n > 0 holds
( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A )
let A be Matrix of REAL; ::_thesis: ( len A = n & width A = m & n > 0 implies ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) )
assume that
A1: ( len A = n & width A = m ) and
A2: n > 0 ; ::_thesis: ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A )
reconsider D = MXR2MXF A as Matrix of n,m,F_Real by A1, A2, MATRIX_1:20;
 ( len (0. (F_Real,n,m)) = n & width (0. (F_Real,n,m)) = m ) by A2, MATRIX_1:23;
then A3: (0_Rmatrix (n,m)) + A = MXF2MXR (D + (0. (F_Real,n,m))) by A1, MATRIX_3:2
.= A by MATRIX_3:4 ;
 MXR2MXF A is Matrix of n,m,F_Real by A1, A2, MATRIX_1:20;
hence  ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) by A3, MATRIX_3:4; ::_thesis: verum
end;

theorem :: MATRIXR1:37
for A, B being Matrix of REAL st len A = len B & width A = width B & A = A + B holds
B = 0_Rmatrix ((len A),(width A))
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & A = A + B implies B = 0_Rmatrix ((len A),(width A)) )
assume that
A1: ( len A = len B & width A = width B ) and
A2: A = A + B ; ::_thesis: B = 0_Rmatrix ((len A),(width A))
0_Rmatrix ((len A),(width A)) = (A + B) + (- A) by A2, MATRIX_4:2
.= MXF2MXR (((MXR2MXF B) + (MXR2MXF A)) + (- (MXR2MXF A))) by A1, MATRIX_3:2
.= MXF2MXR (((MXR2MXF B) + (MXR2MXF A)) - (MXR2MXF A)) by MATRIX_4:def_1
.= B by A1, MATRIX_4:21 ;
hence  B = 0_Rmatrix ((len A),(width A)) ; ::_thesis: verum
end;

theorem :: MATRIXR1:38
for A, B being Matrix of REAL st len A = len B & width A = width B & A + B = 0_Rmatrix ((len A),(width A)) holds
B = - A
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & A + B = 0_Rmatrix ((len A),(width A)) implies B = - A )
assume that
A1: ( len A = len B & width A = width B ) and
A2: A + B = 0_Rmatrix ((len A),(width A)) ; ::_thesis: B = - A
A3: ( len (- (MXR2MXF B)) = len (MXR2MXF B) & width (- (MXR2MXF B)) = width (MXR2MXF B) ) by MATRIX_3:def_2;
MXR2MXF (0_Rmatrix ((len A),(width A))) = (MXR2MXF A) + (- (- (MXR2MXF B))) by A2, MATRIX_4:1
.= (MXR2MXF A) - (- (MXR2MXF B)) by MATRIX_4:def_1 ;
then  MXR2MXF A = - (MXR2MXF B) by A1, A3, MATRIX_4:7;
hence  B = - A by MATRIX_4:1; ::_thesis: verum
end;

theorem :: MATRIXR1:39
for A, B being Matrix of REAL st len A = len B & width A = width B & B - A = B holds
A = 0_Rmatrix ((len A),(width A))
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & B - A = B implies A = 0_Rmatrix ((len A),(width A)) )
assume that
A1: ( len A = len B & width A = width B ) and
A2: B - A = B ; ::_thesis: A = 0_Rmatrix ((len A),(width A))
 (MXR2MXF B) + (MXR2MXF A) = MXR2MXF B by A1, A2, MATRIX_4:22;
hence  A = 0_Rmatrix ((len A),(width A)) by A1, MATRIX_4:6; ::_thesis: verum
end;

theorem Th40: :: MATRIXR1:40
for a being Real
for A, B being Matrix of REAL st width A = len B holds
A * (a * B) = a * (A * B)
proof
let a be Real; ::_thesis: for A, B being Matrix of REAL st width A = len B holds
A * (a * B) = a * (A * B)
let A, B be Matrix of REAL; ::_thesis: ( width A = len B implies A * (a * B) = a * (A * B) )
assume A1: width A = len B ; ::_thesis: A * (a * B) = a * (A * B)
reconsider ea = a as Element of F_Real ;
thus A * (a * B) = MXF2MXR ((MXR2MXF A) * (MXR2MXF (MXF2MXR (ea * (MXR2MXF B))))) by Def7
.= MXF2MXR (ea * (MXR2MXF (MXF2MXR ((MXR2MXF A) * (MXR2MXF B))))) by A1, Th22
.= a * (A * B) by Def7 ; ::_thesis: verum
end;

theorem :: MATRIXR1:41
for a being Real
for A, B being Matrix of REAL st width A = len B & len A > 0 & len B > 0 & width B > 0 holds
(a * A) * B = a * (A * B)
proof
let a be Real; ::_thesis: for A, B being Matrix of REAL st width A = len B & len A > 0 & len B > 0 & width B > 0 holds
(a * A) * B = a * (A * B)
let A, B be Matrix of REAL; ::_thesis: ( width A = len B & len A > 0 & len B > 0 & width B > 0 implies (a * A) * B = a * (A * B) )
assume that
A1: width A = len B and
A2: len A > 0 and
A3: len B > 0 and
A4: width B > 0 ; ::_thesis: (a * A) * B = a * (A * B)
 ( len (A @) = width A & width (B @) = len B ) by A1, A3, A4, MATRIX_2:10;
then  (B @) * (a * (A @)) = a * ((B @) * (A @)) by A1, Th40;
then A5: (B @) * (a * (A @)) = a * ((A * B) @) by A1, A4, MATRIX_3:22;
A6: width (a * (A * B)) = width (A * B) by Th27
.= width B by A1, MATRIX_3:def_4 ;
A7: len (a * (A * B)) = len (A * B) by Th27
.= len A by A1, MATRIX_3:def_4 ;
A8: len (a * A) = len A by Th27;
A9: width (a * A) = width A by Th27;
 width (A * B) = width B by A1, MATRIX_3:def_4;
then  (B @) * (a * (A @)) = (a * (A * B)) @ by A4, A5, Th30;
then  (B @) * ((a * A) @) = (a * (A * B)) @ by A1, A3, Th30;
then A10: ((a * A) * B) @ = (a * (A * B)) @ by A1, A4, A9, MATRIX_3:22;
 ( len ((a * A) * B) = len (a * A) & width ((a * A) * B) = width B ) by A1, A9, MATRIX_3:def_4;
then  (a * A) * B = ((a * (A * B)) @) @ by A2, A4, A8, A10, MATRIX_2:13;
hence  (a * A) * B = a * (A * B) by A2, A4, A7, A6, MATRIX_2:13; ::_thesis: verum
end;

theorem :: MATRIXR1:42
for M being Matrix of REAL holds M + (0_Rmatrix ((len M),(width M))) = M
proof
let M be Matrix of REAL; ::_thesis: M + (0_Rmatrix ((len M),(width M))) = M
A1: ( len M = len (MXR2MXF M) & width M = width (MXR2MXF M) ) ;
M + (0_Rmatrix ((len M),(width M))) = M + (- (0_Rmatrix ((len M),(width M)))) by MATRIX_4:9
.= M + (- (M - M)) by MATRIX_4:3
.= MXF2MXR ((MXR2MXF M) - ((MXR2MXF M) - (MXR2MXF M))) by MATRIX_4:def_1
.= M by A1, MATRIX_4:11 ;
hence  M + (0_Rmatrix ((len M),(width M))) = M ; ::_thesis: verum
end;

theorem :: MATRIXR1:43
for a being real number
for A, B being Matrix of REAL st len A = len B & width A = width B holds
a * (A + B) = (a * A) + (a * B)
proof
let a be real number ; ::_thesis: for A, B being Matrix of REAL st len A = len B & width A = width B holds
a * (A + B) = (a * A) + (a * B)
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B implies a * (A + B) = (a * A) + (a * B) )
assume A1: ( len A = len B & width A = width B ) ; ::_thesis: a * (A + B) = (a * A) + (a * B)
reconsider ea = a as Element of F_Real by XREAL_0:def_1;
A2: (a * A) + (a * B) = MXF2MXR ((MXR2MXF (MXF2MXR (ea * (MXR2MXF A)))) + (MXR2MXF (a * B))) by Def7
.= MXF2MXR ((ea * (MXR2MXF A)) + (MXR2MXF (MXF2MXR (ea * (MXR2MXF B))))) by Def7
.= MXF2MXR ((ea * (MXR2MXF A)) + (ea * (MXR2MXF B))) ;
a * (A + B) = MXF2MXR (ea * (MXR2MXF (A + B))) by Def7
.= MXF2MXR ((ea * (MXR2MXF A)) + (ea * (MXR2MXF B))) by A1, MATRIX_5:20 ;
hence  a * (A + B) = (a * A) + (a * B) by A2; ::_thesis: verum
end;

theorem :: MATRIXR1:44
for A being Matrix of REAL st len A > 0 holds
0 * A = 0_Rmatrix ((len A),(width A))
proof
let A be Matrix of REAL; ::_thesis: ( len A > 0 implies 0 * A = 0_Rmatrix ((len A),(width A)) )
assume A1: len A > 0 ; ::_thesis: 0 * A = 0_Rmatrix ((len A),(width A))
0 * A = MXF2MXR ((0. F_Real) * (MXR2MXF A)) by Def7
.= 0_Rmatrix ((len A),(width A)) by A1, MATRIX_5:24 ;
hence  0 * A = 0_Rmatrix ((len A),(width A)) ; ::_thesis: verum
end;

definition
let x be FinSequence of REAL ;
assume A1: len x > 0 ;
func ColVec2Mx x ->  Matrix of REAL means :Def9: :: MATRIXR1:def 9
( len it = len x & width it = 1 & ( for j being Nat st j in dom x holds
it . j = <*(x . j)*> ) );
existence
 ex b1 being Matrix of REAL st
( len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds
b1 . j = <*(x . j)*> ) )
proof
reconsider n = len x as Element of NAT ;
deffunc H1( Nat) ->  FinSequence of REAL = <*(x . $1)*>;
consider C being FinSequence such that
A2: ( len C = n & ( for j being Nat st j in dom C holds
C . j = H1(j) ) ) from FINSEQ_1:sch_2();
 for y being set st y in rng C holds
ex p being FinSequence of REAL st
( y = p & len p = 1 )
proof
let y be set ; ::_thesis: ( y in rng C implies ex p being FinSequence of REAL st
( y = p & len p = 1 ) )
assume  y in rng C ; ::_thesis: ex p being FinSequence of REAL st
( y = p & len p = 1 )
then consider z being set  such that
A3: z in dom C and
A4: y = C . z by FUNCT_1:def_3;
reconsider z = z as Element of NAT by A3;
 len <*(x . z)*> = 1 by FINSEQ_1:39;
hence  ex p being FinSequence of REAL st
( y = p & len p = 1 ) by A2, A3, A4; ::_thesis: verum
end;
then reconsider B = C as Matrix of REAL by MATRIX_1:9;
 for p being FinSequence of REAL st p in rng B holds
len p = 1
proof
let p be FinSequence of REAL ; ::_thesis: ( p in rng B implies len p = 1 )
assume  p in rng B ; ::_thesis: len p = 1
then consider i being Nat such that
A5: ( i in dom B & B . i = p ) by FINSEQ_2:10;
 len <*(x . i)*> = 1 by FINSEQ_1:39;
hence  len p = 1 by A2, A5; ::_thesis: verum
end;
then reconsider A = B as Matrix of len B,1, REAL by MATRIX_1:def_2;
A6: Seg (len x) = dom x by FINSEQ_1:def_3;
 ( dom C = Seg n & width A = 1 ) by A1, A2, FINSEQ_1:def_3, MATRIX_1:23;
hence  ex b1 being Matrix of REAL st
( len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds
b1 . j = <*(x . j)*> ) ) by A2, A6; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Matrix of REAL st len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds
b1 . j = <*(x . j)*> ) & len b2 = len x & width b2 = 1 & ( for j being Nat st j in dom x holds
b2 . j = <*(x . j)*> ) holds
b1 = b2
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len x & width A = 1 & ( for j being Nat st j in dom x holds
A . j = <*(x . j)*> ) & len B = len x & width B = 1 & ( for j being Nat st j in dom x holds
B . j = <*(x . j)*> ) implies A = B )
assume that
A7: len A = len x and
 width A = 1 and
A8: for k being Nat st k in dom x holds
A . k = <*(x . k)*> and
A9: len B = len x and
 width B = 1 and
A10: for k being Nat st k in dom x holds
B . k = <*(x . k)*> ; ::_thesis: A = B
A11: now__::_thesis:_for_k_being_Nat_st_k_in_dom_x_holds_
A_._k_=_B_._k
let k be Nat; ::_thesis: ( k in dom x implies A . k = B . k )
assume A12: k in dom x ; ::_thesis: A . k = B . k
hence A . k = <*(x . k)*> by A8
.= B . k by A10, A12 ;
::_thesis: verum
end;
 ( dom A = dom x & dom B = dom x ) by A7, A9, FINSEQ_3:29;
hence  A = B by A11, FINSEQ_1:13; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines ColVec2Mx MATRIXR1:def_9_:_
 for x being FinSequence of REAL st len x > 0 holds
for b2 being Matrix of REAL holds
( b2 = ColVec2Mx x iff ( len b2 = len x & width b2 = 1 & ( for j being Nat st j in dom x holds
b2 . j = <*(x . j)*> ) ) );

theorem :: MATRIXR1:45
for x being FinSequence of REAL
for M being Matrix of REAL st len x > 0 holds
( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) )
proof
let x be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL st len x > 0 holds
( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) )
let M be Matrix of REAL; ::_thesis: ( len x > 0 implies ( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) ) )
consider n being Nat such that
A1: for x being set st x in rng M holds
ex s2 being FinSequence st
( s2 = x & len s2 = n ) by MATRIX_1:def_1;
assume A2: len x > 0 ; ::_thesis: ( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) )
thus  ( M = ColVec2Mx x implies ( Col (M,1) = x & width M = 1 ) ) ::_thesis: ( Col (M,1) = x & width M = 1 implies M = ColVec2Mx x )
proof
assume A3: M = ColVec2Mx x ; ::_thesis: ( Col (M,1) = x & width M = 1 )
then A4: width M = 1 by A2, Def9;
A5: len M = len x by A2, A3, Def9;
then A6: dom M = dom x by FINSEQ_3:29;
 for j being Nat st j in dom M holds
x . j = M * (j,1)
proof
let j be Nat; ::_thesis: ( j in dom M implies x . j = M * (j,1) )
assume A7: j in dom M ; ::_thesis: x . j = M * (j,1)
then reconsider j = j as Element of NAT ;
A8: M . j = <*(x . j)*> by A2, A3, A6, A7, Def9;
then reconsider q = M . j as FinSequence of REAL ;
A9: q . 1 = x . j by A8, FINSEQ_1:40;
 1 in Seg (width M) by A4, FINSEQ_1:1;
then  [j,1] in Indices M by A7, ZFMISC_1:87;
hence  x . j = M * (j,1) by A9, MATRIX_1:def_5; ::_thesis: verum
end;
hence  ( Col (M,1) = x & width M = 1 ) by A2, A3, A5, Def9, MATRIX_1:def_8; ::_thesis: verum
end;
assume that
A10: Col (M,1) = x and
A11: width M = 1 ; ::_thesis: M = ColVec2Mx x
A12: len x = len M by A10, MATRIX_1:def_8;
then consider s being FinSequence such that
A13: s in rng M and
A14: len s = 1 by A2, A11, MATRIX_1:def_3;
A15: dom x = dom M by A12, FINSEQ_3:29;
A16: ex s2 being FinSequence st
( s2 = s & len s2 = n ) by A13, A1;
 for j being Nat st j in dom x holds
M . j = <*(x . j)*>
proof
let j be Nat; ::_thesis: ( j in dom x implies M . j = <*(x . j)*> )
assume A17: j in dom x ; ::_thesis: M . j = <*(x . j)*>
then  M . j in rng M by A15, FUNCT_1:def_3;
then A18: ex s3 being FinSequence st
( s3 = M . j & len s3 = 1 ) by A14, A1, A16;
 1 in Seg (width M) by A11, FINSEQ_1:1;
then  [j,1] in Indices M by A15, A17, ZFMISC_1:87;
then A19: ex p being FinSequence of REAL st
( p = M . j & M * (j,1) = p . 1 ) by MATRIX_1:def_5;
 x . j = M * (j,1) by A10, A15, A17, MATRIX_1:def_8;
hence  M . j = <*(x . j)*> by A19, A18, FINSEQ_1:40; ::_thesis: verum
end;
hence  M = ColVec2Mx x by A2, A11, A12, Def9; ::_thesis: verum
end;

theorem Th46: :: MATRIXR1:46
for x1, x2 being 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 ; ::_thesis: ( len x1 = len x2 & len x1 > 0 implies ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2) )
assume that
A1: len x1 = len x2 and
A2: len x1 > 0 ; ::_thesis: ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2)
A3: width (ColVec2Mx x1) = 1 by A2, Def9;
A4: Seg (width (ColVec2Mx x1)) = Seg 1 by A2, Def9;
A5: dom x1 = dom x2 by A1, FINSEQ_3:29;
A6: len (ColVec2Mx x1) = len x1 by A2, Def9;
then A7: dom (ColVec2Mx x1) = dom x1 by FINSEQ_3:29;
 ( len (ColVec2Mx x2) = len x2 & width (ColVec2Mx x2) = 1 ) by A1, A2, Def9;
then A8: Indices (ColVec2Mx x2) = Indices (ColVec2Mx x1) by A1, A6, A3, MATRIX_4:55;
A9: len (x1 + x2) = len x1 by A1, RVSUM_1:115;
then A10: dom (x1 + x2) = dom x1 by FINSEQ_3:29;
A11: ( len (ColVec2Mx (x1 + x2)) = len (x1 + x2) & width (ColVec2Mx (x1 + x2)) = 1 ) by A2, A9, Def9;
then A12: Indices (ColVec2Mx (x1 + x2)) = Indices (ColVec2Mx x1) by A1, A6, A3, MATRIX_4:55, RVSUM_1:115;
 for i, j being Nat 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 be Nat; ::_thesis: ( [i,j] in Indices (ColVec2Mx x1) implies (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) )
thus  ( [i,j] in Indices (ColVec2Mx x1) implies (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) ) ::_thesis: verum
proof
assume A13: [i,j] in Indices (ColVec2Mx x1) ; ::_thesis: (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j))
then consider q1 being FinSequence of REAL  such that
A14: q1 = (ColVec2Mx x1) . i and
A15: (ColVec2Mx x1) * (i,j) = q1 . j by MATRIX_1:def_5;
 j in Seg 1 by A4, A13, ZFMISC_1:87;
then  ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A16: j = 1 by XXREAL_0:1;
A17: i in dom x1 by A7, A13, ZFMISC_1:87;
then  (ColVec2Mx x1) . i = <*(x1 . i)*> by A2, Def9;
then A18: q1 . j = x1 . i by A16, A14, FINSEQ_1:40;
consider p being FinSequence of REAL  such that
A19: p = (ColVec2Mx (x1 + x2)) . i and
A20: (ColVec2Mx (x1 + x2)) * (i,j) = p . j by A12, A13, MATRIX_1:def_5;
consider q2 being FinSequence of REAL  such that
A21: q2 = (ColVec2Mx x2) . i and
A22: (ColVec2Mx x2) * (i,j) = q2 . j by A8, A13, MATRIX_1:def_5;
 (ColVec2Mx x2) . i = <*(x2 . i)*> by A1, A2, A5, A17, Def9;
then A23: q2 . j = x2 . i by A16, A21, FINSEQ_1:40;
 (ColVec2Mx (x1 + x2)) . i = <*((x1 + x2) . i)*> by A2, A9, A10, A17, Def9;
then  p . j = (x1 + x2) . i by A16, A19, FINSEQ_1:40;
hence  (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) by A10, A17, A20, A15, A18, A22, A23, VALUED_1:def_1; ::_thesis: verum
end;
end;
hence  ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2) by A1, A6, A11, A3, Th26, RVSUM_1:115; ::_thesis: verum
end;

theorem Th47: :: MATRIXR1:47
for a being Real
for x being FinSequence of REAL st len x > 0 holds
ColVec2Mx (a * x) = a * (ColVec2Mx x)
proof
let a be Real; ::_thesis: for x being FinSequence of REAL st len x > 0 holds
ColVec2Mx (a * x) = a * (ColVec2Mx x)
let x be FinSequence of REAL ; ::_thesis: ( len x > 0 implies ColVec2Mx (a * x) = a * (ColVec2Mx x) )
assume A1: len x > 0 ; ::_thesis: ColVec2Mx (a * x) = a * (ColVec2Mx x)
A2: len (a * (ColVec2Mx x)) = len (ColVec2Mx x) by Th27
.= len x by A1, Def9 ;
A3: len (a * x) = len x by RVSUM_1:117;
then A4: dom (a * x) = dom x by FINSEQ_3:29;
A5: for j being Nat st j in dom (a * x) holds
(a * (ColVec2Mx x)) . j = <*((a * x) . j)*>
proof
 len (ColVec2Mx x) = len x by A1, Def9;
then A6: dom (ColVec2Mx x) = dom x by FINSEQ_3:29;
let j be Nat; ::_thesis: ( j in dom (a * x) implies (a * (ColVec2Mx x)) . j = <*((a * x) . j)*> )
consider n being Nat such that
A7: for x2 being set st x2 in rng (a * (ColVec2Mx x)) holds
ex s2 being FinSequence st
( s2 = x2 & len s2 = n ) by MATRIX_1:def_1;
assume A8: j in dom (a * x) ; ::_thesis: (a * (ColVec2Mx x)) . j = <*((a * x) . j)*>
then A9: (ColVec2Mx x) . j = <*(x . j)*> by A1, A4, Def9;
A10: j in dom (a * (ColVec2Mx x)) by A2, A3, A8, FINSEQ_3:29;
then  (a * (ColVec2Mx x)) . j in rng (a * (ColVec2Mx x)) by FUNCT_1:def_3;
then reconsider q = (a * (ColVec2Mx x)) . j as FinSequence of REAL by FINSEQ_1:def_11;
 q in rng (a * (ColVec2Mx x)) by A10, FUNCT_1:def_3;
then A11: ex s2 being FinSequence st
( s2 = q & len s2 = n ) by A7;
consider s being FinSequence such that
A12: s in rng (a * (ColVec2Mx x)) and
A13: len s = width (a * (ColVec2Mx x)) by A1, A2, MATRIX_1:def_3;
 ex s3 being FinSequence st
( s3 = s & len s3 = n ) by A12, A7;
then A14: len q = width (ColVec2Mx x) by A13, A11, Th27
.= 1 by A1, Def9
.= len <*((a * x) . j)*> by FINSEQ_1:40 ;
 width (ColVec2Mx x) = 1 by A1, Def9;
then A15: 1 in Seg (width (MXR2MXF (ColVec2Mx x))) by FINSEQ_1:1;
 j in dom x by A3, A8, FINSEQ_3:29;
then A16: [j,1] in Indices (MXR2MXF (ColVec2Mx x)) by A6, A15, ZFMISC_1:87;
then A17: ex p3 being FinSequence of REAL st
( p3 = (ColVec2Mx x) . j & (ColVec2Mx x) * (j,1) = p3 . 1 ) by MATRIX_1:def_5;
 [j,1] in Indices (a * (ColVec2Mx x)) by A16, Th28;
then A18: ex p being FinSequence of REAL st
( p = (a * (ColVec2Mx x)) . j & (a * (ColVec2Mx x)) * (j,1) = p . 1 ) by MATRIX_1:def_5;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A19: q . 1 = a * ((ColVec2Mx x) * (j,1)) by A16, A18, Th29
.= a * (x . j) by A17, A9, FINSEQ_1:40
.= (a * x) . j by RVSUM_1:44
.= <*((a * x) . j)*> . 1 by FINSEQ_1:40 ;
 for i being Nat st 1 <= i & i <= len <*((a * x) . j)*> holds
q . i = <*((a * x) . j)*> . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len <*((a * x) . j)*> implies q . i = <*((a * x) . j)*> . i )
A20: len <*((a * x) . j)*> = 1 by FINSEQ_1:40;
assume  ( 1 <= i & i <= len <*((a * x) . j)*> ) ; ::_thesis: q . i = <*((a * x) . j)*> . i
then  i = 1 by A20, XXREAL_0:1;
hence  q . i = <*((a * x) . j)*> . i by A19; ::_thesis: verum
end;
hence  (a * (ColVec2Mx x)) . j = <*((a * x) . j)*> by A14, FINSEQ_1:14; ::_thesis: verum
end;
width (a * (ColVec2Mx x)) = width (ColVec2Mx x) by Th27
.= 1 by A1, Def9 ;
hence  ColVec2Mx (a * x) = a * (ColVec2Mx x) by A1, A2, A3, A5, Def9; ::_thesis: verum
end;

definition
let x be FinSequence of REAL ;
func LineVec2Mx x ->  Matrix of REAL means :Def10: :: MATRIXR1:def 10
( width it = len x & len it = 1 & ( for j being Nat st j in dom x holds
it * (1,j) = x . j ) );
existence
 ex b1 being Matrix of REAL st
( width b1 = len x & len b1 = 1 & ( for j being Nat st j in dom x holds
b1 * (1,j) = x . j ) )
proof
set B = <*x*>;
A1: rng <*x*> = {x} by FINSEQ_1:39;
 for y being set st y in rng <*x*> holds
ex p being FinSequence of REAL st
( y = p & len p = len x )
proof
let y be set ; ::_thesis: ( y in rng <*x*> implies ex p being FinSequence of REAL st
( y = p & len p = len x ) )
assume  y in rng <*x*> ; ::_thesis: ex p being FinSequence of REAL st
( y = p & len p = len x )
then  y = x by A1, TARSKI:def_1;
hence  ex p being FinSequence of REAL st
( y = p & len p = len x ) ; ::_thesis: verum
end;
then reconsider C = <*x*> as Matrix of REAL by MATRIX_1:9;
take  C ; ::_thesis: ( width C = len x & len C = 1 & ( for j being Nat st j in dom x holds
C * (1,j) = x . j ) )
A2: len <*x*> = 1 by FINSEQ_1:39;
then  dom C = Seg 1 by FINSEQ_1:def_3;
then A3: 1 in dom C by FINSEQ_1:1;
 for p being FinSequence of REAL st p in rng C holds
len p = len x by A1, TARSKI:def_1;
then  ( len <*x*> = 1 & C is Matrix of 1, len x, REAL ) by A2, MATRIX_1:def_2;
hence A4: width C = len x by MATRIX_1:20; ::_thesis: ( len C = 1 & ( for j being Nat st j in dom x holds
C * (1,j) = x . j ) )
thus  len C = 1 by FINSEQ_1:40; ::_thesis: for j being Nat st j in dom x holds
C * (1,j) = x . j
let j be Nat; ::_thesis: ( j in dom x implies C * (1,j) = x . j )
assume  j in dom x ; ::_thesis: C * (1,j) = x . j
then  j in Seg (len x) by FINSEQ_1:def_3;
then  ( <*x*> . 1 = x & [1,j] in Indices C ) by A4, A3, FINSEQ_1:40, ZFMISC_1:def_2;
hence  C * (1,j) = x . j by MATRIX_1:def_5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Matrix of REAL st width b1 = len x & len b1 = 1 & ( for j being Nat st j in dom x holds
b1 * (1,j) = x . j ) & width b2 = len x & len b2 = 1 & ( for j being Nat st j in dom x holds
b2 * (1,j) = x . j ) holds
b1 = b2
proof
let A, B be Matrix of REAL; ::_thesis: ( width A = len x & len A = 1 & ( for j being Nat st j in dom x holds
A * (1,j) = x . j ) & width B = len x & len B = 1 & ( for j being Nat st j in dom x holds
B * (1,j) = x . j ) implies A = B )
assume that
A5: width A = len x and
A6: len A = 1 and
A7: for k being Nat st k in dom x holds
A * (1,k) = x . k and
A8: ( width B = len x & len B = 1 ) and
A9: for k being Nat st k in dom x holds
B * (1,k) = x . k ; ::_thesis: A = B
A10: dom A = Seg 1 by A6, FINSEQ_1:def_3;
 for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies A * (i,j) = B * (i,j) )
assume A11: [i,j] in Indices A ; ::_thesis: A * (i,j) = B * (i,j)
then  i in Seg 1 by A10, ZFMISC_1:87;
then  ( 1 <= i & i <= 1 ) by FINSEQ_1:1;
then A12: i = 1 by XXREAL_0:1;
 j in Seg (len x) by A5, A11, ZFMISC_1:87;
then A13: j in dom x by FINSEQ_1:def_3;
then  A * (i,j) = x . j by A7, A12;
hence  A * (i,j) = B * (i,j) by A9, A13, A12; ::_thesis: verum
end;
hence  A = B by A5, A6, A8, MATRIX_1:21; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines LineVec2Mx MATRIXR1:def_10_:_
 for x being FinSequence of REAL
for b2 being Matrix of REAL holds
( b2 = LineVec2Mx x iff ( width b2 = len x & len b2 = 1 & ( for j being Nat st j in dom x holds
b2 * (1,j) = x . j ) ) );

theorem :: MATRIXR1:48
for x being FinSequence of REAL
for M being Matrix of REAL holds
( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) )
proof
let x be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL holds
( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) )
let M be Matrix of REAL; ::_thesis: ( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) )
thus  ( M = LineVec2Mx x implies ( Line (M,1) = x & len M = 1 ) ) ::_thesis: ( Line (M,1) = x & len M = 1 implies M = LineVec2Mx x )
proof
assume A1: M = LineVec2Mx x ; ::_thesis: ( Line (M,1) = x & len M = 1 )
then A2: for j being Nat st j in dom x holds
M * (1,j) = x . j by Def10;
A3: width M = len x by A1, Def10;
then  dom x = Seg (width M) by FINSEQ_1:def_3;
hence  ( Line (M,1) = x & len M = 1 ) by A1, A3, A2, Def10, MATRIX_1:def_7; ::_thesis: verum
end;
assume that
A4: Line (M,1) = x and
A5: len M = 1 ; ::_thesis: M = LineVec2Mx x
A6: for j being Nat st j in Seg (width M) holds
x . j = M * (1,j) by A4, MATRIX_1:def_7;
A7: len x = width M by A4, MATRIX_1:def_7;
then  Seg (width M) = dom x by FINSEQ_1:def_3;
hence  M = LineVec2Mx x by A5, A7, A6, Def10; ::_thesis: verum
end;

theorem Th49: :: MATRIXR1:49
for x being FinSequence of REAL st len x > 0 holds
( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x )
proof
let x be FinSequence of REAL ; ::_thesis: ( len x > 0 implies ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x ) )
A1: dom (LineVec2Mx x) = Seg (len (LineVec2Mx x)) by FINSEQ_1:def_3;
A2: width (LineVec2Mx x) = len x by Def10;
assume A3: len x > 0 ; ::_thesis: ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x )
then A4: len (ColVec2Mx x) = len x by Def9;
A5: len (LineVec2Mx x) = 1 by Def10;
A6: width (ColVec2Mx x) = 1 by A3, Def9;
A7: dom (ColVec2Mx x) = Seg (len (ColVec2Mx x)) by FINSEQ_1:def_3;
A8: for i, j being Nat holds
( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) )
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) )
 ( [i,j] in Indices (ColVec2Mx x) iff ( i in dom (ColVec2Mx x) & j in Seg (width (ColVec2Mx x)) ) ) by ZFMISC_1:87;
hence  ( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) ) by A2, A5, A4, A6, A7, A1, ZFMISC_1:87; ::_thesis: verum
end;
A9: for i, j being Nat st [j,i] in Indices (LineVec2Mx x) holds
(ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i)
proof
let i, j be Nat; ::_thesis: ( [j,i] in Indices (LineVec2Mx x) implies (ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i) )
assume A10: [j,i] in Indices (LineVec2Mx x) ; ::_thesis: (ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i)
then  [i,j] in Indices (ColVec2Mx x) by A8;
then A11: ex p being FinSequence of REAL st
( p = (ColVec2Mx x) . i & (ColVec2Mx x) * (i,j) = p . j ) by MATRIX_1:def_5;
 j in Seg 1 by A5, A1, A10, ZFMISC_1:87;
then  ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A12: j = 1 by XXREAL_0:1;
 i in Seg (len x) by A2, A10, ZFMISC_1:87;
then A13: i in dom x by FINSEQ_1:def_3;
then  (ColVec2Mx x) . i = <*(x . i)*> by A3, Def9;
hence (ColVec2Mx x) * (i,j) = x . i by A12, A11, FINSEQ_1:40
.= (LineVec2Mx x) * (j,i) by A12, A13, Def10 ;
::_thesis: verum
end;
hence  (LineVec2Mx x) @ = ColVec2Mx x by A2, A4, A8, MATRIX_1:def_6; ::_thesis: (ColVec2Mx x) @ = LineVec2Mx x
A14: for i, j being Nat st [j,i] in Indices (ColVec2Mx x) holds
(LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i)
proof
let i, j be Nat; ::_thesis: ( [j,i] in Indices (ColVec2Mx x) implies (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i) )
assume  [j,i] in Indices (ColVec2Mx x) ; ::_thesis: (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i)
then  [i,j] in Indices (LineVec2Mx x) by A8;
hence  (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i) by A9; ::_thesis: verum
end;
 for i, j being Nat holds
( [i,j] in Indices (LineVec2Mx x) iff [j,i] in Indices (ColVec2Mx x) ) by A8;
hence  (ColVec2Mx x) @ = LineVec2Mx x by A5, A6, A14, MATRIX_1:def_6; ::_thesis: verum
end;

theorem Th50: :: MATRIXR1:50
for x1, x2 being FinSequence of REAL st len x1 = len x2 holds
LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2)
proof
let x1, x2 be FinSequence of REAL ; ::_thesis: ( len x1 = len x2 implies LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) )
assume A1: len x1 = len x2 ; ::_thesis: LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2)
then A2: dom x1 = dom x2 by FINSEQ_3:29;
 len (x1 + x2) = len x1 by A1, RVSUM_1:115;
then A3: dom (x1 + x2) = dom x1 by FINSEQ_3:29;
A4: ( width (LineVec2Mx x1) = len x1 & len (LineVec2Mx x1) = 1 ) by Def10;
 ( width (LineVec2Mx x2) = len x2 & len (LineVec2Mx x2) = 1 ) by Def10;
then A5: Indices (LineVec2Mx x2) = Indices (LineVec2Mx x1) by A1, A4, MATRIX_4:55;
A6: Seg (width (LineVec2Mx x1)) = Seg (len x1) by Def10
.= dom x1 by FINSEQ_1:def_3 ;
A7: dom (LineVec2Mx x1) = Seg (len (LineVec2Mx x1)) by FINSEQ_1:def_3
.= Seg 1 by Def10 ;
A8: ( width (LineVec2Mx (x1 + x2)) = len (x1 + x2) & len (LineVec2Mx (x1 + x2)) = 1 ) by Def10;
then A9: Indices (LineVec2Mx (x1 + x2)) = Indices (LineVec2Mx x1) by A1, A4, MATRIX_4:55, RVSUM_1:115;
 for i, j being Nat st [i,j] in Indices (LineVec2Mx x1) holds
(LineVec2Mx (x1 + x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (LineVec2Mx x1) implies (LineVec2Mx (x1 + x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j)) )
assume A10: [i,j] in Indices (LineVec2Mx x1) ; ::_thesis: (LineVec2Mx (x1 + x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j))
then consider q1 being FinSequence of REAL  such that
 q1 = (LineVec2Mx x1) . i and
A11: (LineVec2Mx x1) * (i,j) = q1 . j by MATRIX_1:def_5;
consider p being FinSequence of REAL  such that
 p = (LineVec2Mx (x1 + x2)) . i and
A12: (LineVec2Mx (x1 + x2)) * (i,j) = p . j by A9, A10, MATRIX_1:def_5;
consider q2 being FinSequence of REAL  such that
 q2 = (LineVec2Mx x2) . i and
A13: (LineVec2Mx x2) * (i,j) = q2 . j by A5, A10, MATRIX_1:def_5;
A14: j in dom x1 by A6, A10, ZFMISC_1:87;
 i in Seg 1 by A7, A10, ZFMISC_1:87;
then  ( 1 <= i & i <= 1 ) by FINSEQ_1:1;
then A15: i = 1 by XXREAL_0:1;
then A16: q1 . j = x1 . j by A14, A11, Def10;
A17: q2 . j = x2 . j by A2, A14, A15, A13, Def10;
 p . j = (x1 + x2) . j by A3, A14, A15, A12, Def10;
hence  (LineVec2Mx (x1 + x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j)) by A3, A14, A12, A11, A16, A13, A17, VALUED_1:def_1; ::_thesis: verum
end;
hence  LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) by A1, A8, A4, Th26, RVSUM_1:115; ::_thesis: verum
end;

theorem :: MATRIXR1:51
for a being Real
for x being FinSequence of REAL holds LineVec2Mx (a * x) = a * (LineVec2Mx x)
proof
let a be Real; ::_thesis: for x being FinSequence of REAL holds LineVec2Mx (a * x) = a * (LineVec2Mx x)
let x be FinSequence of REAL ; ::_thesis: LineVec2Mx (a * x) = a * (LineVec2Mx x)
A1: len (a * (LineVec2Mx x)) = len (LineVec2Mx x) by Th27
.= 1 by Def10 ;
A2: len (a * x) = len x by RVSUM_1:117;
then A3: dom (a * x) = dom x by FINSEQ_3:29;
A4: for j being Nat st j in dom (a * x) holds
(a * (LineVec2Mx x)) * (1,j) = (a * x) . j
proof
 len (LineVec2Mx x) = 1 by Def10;
then  1 in Seg (len (LineVec2Mx x)) by FINSEQ_1:1;
then A5: 1 in dom (LineVec2Mx x) by FINSEQ_1:def_3;
 1 in Seg (len (a * (LineVec2Mx x))) by A1, FINSEQ_1:1;
then  1 in dom (a * (LineVec2Mx x)) by FINSEQ_1:def_3;
then  (a * (LineVec2Mx x)) . 1 in rng (a * (LineVec2Mx x)) by FUNCT_1:def_3;
then reconsider q = (a * (LineVec2Mx x)) . 1 as FinSequence of REAL by FINSEQ_1:def_11;
let j be Nat; ::_thesis: ( j in dom (a * x) implies (a * (LineVec2Mx x)) * (1,j) = (a * x) . j )
A6: width (LineVec2Mx x) = len x by Def10;
A7: Indices (a * (LineVec2Mx x)) = Indices (LineVec2Mx x) by Th28;
assume A8: j in dom (a * x) ; ::_thesis: (a * (LineVec2Mx x)) * (1,j) = (a * x) . j
then  j in Seg (len x) by A2, FINSEQ_1:def_3;
then A9: [1,j] in Indices (a * (LineVec2Mx x)) by A6, A5, A7, ZFMISC_1:87;
then A10: ex p being FinSequence of REAL st
( p = (a * (LineVec2Mx x)) . 1 & (a * (LineVec2Mx x)) * (1,j) = p . j ) by MATRIX_1:def_5;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
q . j = a * ((LineVec2Mx x) * (1,j)) by A7, A9, A10, Th29
.= a * (x . j) by A3, A8, Def10
.= (a * x) . j by RVSUM_1:44 ;
hence  (a * (LineVec2Mx x)) * (1,j) = (a * x) . j by A9, MATRIX_1:def_5; ::_thesis: verum
end;
width (a * (LineVec2Mx x)) = width (LineVec2Mx x) by Th27
.= len x by Def10 ;
hence  LineVec2Mx (a * x) = a * (LineVec2Mx x) by A1, A2, A4, Def10; ::_thesis: verum
end;

definition
let M be Matrix of REAL;
let x be FinSequence of REAL ;
funcM * x ->  FinSequence of REAL  equals :: MATRIXR1:def 11
 Col ((M * (ColVec2Mx x)),1);
coherence
 Col ((M * (ColVec2Mx x)),1) is FinSequence of REAL ;
funcx * M ->  FinSequence of REAL  equals :: MATRIXR1:def 12
 Line (((LineVec2Mx x) * M),1);
coherence
 Line (((LineVec2Mx x) * M),1) is FinSequence of REAL ;
end;

:: deftheorem  defines * MATRIXR1:def_11_:_
 for M being Matrix of REAL
for x being FinSequence of REAL holds M * x = Col ((M * (ColVec2Mx x)),1);

:: deftheorem  defines * MATRIXR1:def_12_:_
 for M being Matrix of REAL
for x being FinSequence of REAL holds x * M = Line (((LineVec2Mx x) * M),1);

theorem Th52: :: MATRIXR1:52
for x being FinSequence of REAL
for A being Matrix of REAL st len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) holds
(A @) * x = x * A
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) holds
(A @) * x = x * A
let A be Matrix of REAL; ::_thesis: ( len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) implies (A @) * x = x * A )
assume that
A1: len A > 0 and
A2: width A > 0 and
A3: ( len A = len x or width (A @) = len x ) ; ::_thesis: (A @) * x = x * A
A4: len A = len x by A2, A3, MATRIX_2:10;
A5: len A = width (A @) by A2, MATRIX_2:10;
then  len (ColVec2Mx x) = len x by A1, A3, Def9;
then A6: width ((A @) * (ColVec2Mx x)) = width (ColVec2Mx x) by A3, A5, MATRIX_3:def_4;
 width (ColVec2Mx x) = 1 by A1, A3, A5, Def9;
then A7: 1 in Seg (width ((A @) * (ColVec2Mx x))) by A6, FINSEQ_1:1;
A8: len (LineVec2Mx x) = 1 by Def10;
A9: width (LineVec2Mx x) = len x by Def10;
then  width (LineVec2Mx x) = len A by A2, A3, MATRIX_2:10;
then  ( len ((LineVec2Mx x) * A) = len (LineVec2Mx x) & width ((LineVec2Mx x) * A) = width A ) by MATRIX_3:def_4;
then  Line (((LineVec2Mx x) * A),1) = Line (((((LineVec2Mx x) * A) @) @),1) by A2, A8, MATRIX_2:13
.= Line ((((A @) * ((LineVec2Mx x) @)) @),1) by A2, A4, A9, MATRIX_3:22
.= Line ((((A @) * (ColVec2Mx x)) @),1) by A1, A4, Th49
.= Col (((A @) * (ColVec2Mx x)),1) by A7, MATRIX_2:15 ;
hence  (A @) * x = x * A ; ::_thesis: verum
end;

theorem Th53: :: MATRIXR1:53
for x being FinSequence of REAL
for A being Matrix of REAL st len A > 0 & width A > 0 & ( width A = len x or len (A @) = len x ) holds
A * x = x * (A @)
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A > 0 & width A > 0 & ( width A = len x or len (A @) = len x ) holds
A * x = x * (A @)
let A be Matrix of REAL; ::_thesis: ( len A > 0 & width A > 0 & ( width A = len x or len (A @) = len x ) implies A * x = x * (A @) )
assume that
A1: len A > 0 and
A2: width A > 0 and
A3: ( width A = len x or len (A @) = len x ) ; ::_thesis: A * x = x * (A @)
 ( len (A @) = width A & width (A @) = len A ) by A2, MATRIX_2:10;
then  ((A @) @) * x = x * (A @) by A1, A2, A3, Th52;
hence  A * x = x * (A @) by A1, A2, MATRIX_2:13; ::_thesis: verum
end;

theorem Th54: :: MATRIXR1:54
for A, B being Matrix of REAL st len A = len B holds
for i being 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; ::_thesis: ( len A = len B implies for i being Nat st 1 <= i & i <= width A holds
Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) )
assume A1: len A = len B ; ::_thesis: for i being Nat st 1 <= i & i <= width A holds
Col ((A + B),i) = (Col (A,i)) + (Col (B,i))
then A2: dom A = dom B by FINSEQ_3:29;
let i be Nat; ::_thesis: ( 1 <= i & i <= width A implies Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) )
A3: len (Col (A,i)) = len A by MATRIX_1:def_8;
 len (Col (B,i)) = len B by MATRIX_1:def_8;
then A4: len ((Col (A,i)) + (Col (B,i))) = len (Col (A,i)) by A1, A3, RVSUM_1:115;
assume  ( 1 <= i & i <= width A ) ; ::_thesis: Col ((A + B),i) = (Col (A,i)) + (Col (B,i))
then A5: i in Seg (width A) by FINSEQ_1:1;
A6: len (A + B) = len A by Th25;
 Seg (len (A + B)) = dom (A + B) by FINSEQ_1:def_3;
then A7: dom ((Col (A,i)) + (Col (B,i))) = dom (A + B) by A3, A6, A4, FINSEQ_1:def_3;
 for j being Nat st j in dom (A + B) holds
((Col (A,i)) + (Col (B,i))) . j = (A + B) * (j,i)
proof
let j be Nat; ::_thesis: ( j in dom (A + B) implies ((Col (A,i)) + (Col (B,i))) . j = (A + B) * (j,i) )
assume A8: j in dom (A + B) ; ::_thesis: ((Col (A,i)) + (Col (B,i))) . j = (A + B) * (j,i)
then  j in Seg (len (A + B)) by FINSEQ_1:def_3;
then A9: j in dom A by A6, FINSEQ_1:def_3;
then A10: [j,i] in Indices A by A5, ZFMISC_1:87;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
 ( (Col (A,i)) . j = A * (j,i) & (Col (B,i)) . j = B * (j,i) ) by A2, A9, MATRIX_1:def_8;
then  ((Col (A,i)) . j) + ((Col (B,i)) . j) = (A + B) * (j,i) by A10, Th25;
hence  ((Col (A,i)) + (Col (B,i))) . j = (A + B) * (j,i) by A7, A8, VALUED_1:def_1; ::_thesis: verum
end;
hence  Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) by A3, A6, A4, MATRIX_1:def_8; ::_thesis: verum
end;

theorem Th55: :: MATRIXR1:55
for A, B being Matrix of REAL st width A = width B holds
for i being 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; ::_thesis: ( width A = width B implies for i being Nat st 1 <= i & i <= len A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) )
assume A1: width A = width B ; ::_thesis: for i being Nat st 1 <= i & i <= len A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let i be Nat; ::_thesis: ( 1 <= i & i <= len A implies Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) )
A2: len (Line (A,i)) = width A by MATRIX_1:def_7;
assume  ( 1 <= i & i <= len A ) ; ::_thesis: Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
then A3: i in dom A by FINSEQ_3:25;
A4: width (A + B) = width A by Th25;
 len (Line (B,i)) = width B by MATRIX_1:def_7;
then A5: len ((Line (A,i)) + (Line (B,i))) = len (Line (A,i)) by A1, A2, RVSUM_1:115;
then A6: dom ((Line (A,i)) + (Line (B,i))) = Seg (width A) by A2, FINSEQ_1:def_3;
 for j being Nat st j in Seg (width (A + B)) holds
((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j)
proof
let j be Nat; ::_thesis: ( j in Seg (width (A + B)) implies ((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j) )
assume A7: j in Seg (width (A + B)) ; ::_thesis: ((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j)
then A8: j in Seg (width A) by Th25;
then A9: ( [i,j] in Indices A & (Line (A,i)) . j = A * (i,j) ) by A3, MATRIX_1:def_7, ZFMISC_1:87;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
 (Line (B,i)) . j = B * (i,j) by A1, A8, MATRIX_1:def_7;
then  ((Line (A,i)) . j) + ((Line (B,i)) . j) = (A + B) * (i,j) by A9, Th25;
hence  ((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j) by A4, A6, A7, VALUED_1:def_1; ::_thesis: verum
end;
hence  Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) by A2, A4, A5, MATRIX_1:def_7; ::_thesis: verum
end;

theorem Th56: :: MATRIXR1:56
for a being Real
for M being Matrix of REAL
for i being Nat st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
proof
let a be Real; ::_thesis: for M being Matrix of REAL
for i being Nat st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
let M be Matrix of REAL; ::_thesis: for i being Nat st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
reconsider ea = a as Element of F_Real ;
let i be Nat; ::_thesis: ( 1 <= i & i <= width M implies Col ((a * M),i) = a * (Col (M,i)) )
assume A1: ( 1 <= i & i <= width M ) ; ::_thesis: Col ((a * M),i) = a * (Col (M,i))
Col ((a * M),i) = Col ((MXF2MXR (ea * (MXR2MXF M))),i) by Def7
.= ea * (Col ((MXR2MXF M),i)) by A1, Th19 ;
hence  Col ((a * M),i) = a * (Col (M,i)) by Th17; ::_thesis: verum
end;

theorem :: MATRIXR1:57
for x1, x2 being FinSequence of REAL
for A being Matrix of REAL st len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 holds
A * (x1 + x2) = (A * x1) + (A * x2)
proof
let x1, x2 be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 holds
A * (x1 + x2) = (A * x1) + (A * x2)
let A be Matrix of REAL; ::_thesis: ( len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 implies A * (x1 + x2) = (A * x1) + (A * x2) )
assume that
A1: len x1 = len x2 and
A2: width A = len x1 and
A3: len x1 > 0 and
A4: len A > 0 ; ::_thesis: A * (x1 + x2) = (A * x1) + (A * x2)
A5: len (ColVec2Mx x2) = len x2 by A1, A3, Def9;
A6: len (ColVec2Mx x1) = len x1 by A3, Def9;
then A7: len (A * (ColVec2Mx x1)) = len A by A2, MATRIX_3:def_4
.= len (A * (ColVec2Mx x2)) by A1, A2, A5, MATRIX_3:def_4 ;
A8: width (ColVec2Mx x1) = 1 by A3, Def9;
then A9: 1 <= width (A * (ColVec2Mx x1)) by A2, A6, MATRIX_3:def_4;
A10: width (ColVec2Mx x2) = 1 by A1, A3, Def9;
thus A * (x1 + x2) = Col ((A * ((ColVec2Mx x1) + (ColVec2Mx x2))),1) by A1, A3, Th46
.= Col (((A * (ColVec2Mx x1)) + (A * (ColVec2Mx x2))),1) by A1, A2, A3, A4, A6, A5, A8, A10, MATRIX_4:62
.= (A * x1) + (A * x2) by A7, A9, Th54 ; ::_thesis: verum
end;

theorem :: MATRIXR1:58
for x1, x2 being FinSequence of REAL
for A being Matrix of REAL st len x1 = len x2 & len A = len x1 & len x1 > 0 holds
(x1 + x2) * A = (x1 * A) + (x2 * A)
proof
let x1, x2 be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x1 = len x2 & len A = len x1 & len x1 > 0 holds
(x1 + x2) * A = (x1 * A) + (x2 * A)
let A be Matrix of REAL; ::_thesis: ( len x1 = len x2 & len A = len x1 & len x1 > 0 implies (x1 + x2) * A = (x1 * A) + (x2 * A) )
assume that
A1: len x1 = len x2 and
A2: len A = len x1 and
A3: len x1 > 0 ; ::_thesis: (x1 + x2) * A = (x1 * A) + (x2 * A)
A4: width (LineVec2Mx x2) = len x2 by Def10;
A5: width (LineVec2Mx x1) = len x1 by Def10;
then A6: width ((LineVec2Mx x1) * A) = width A by A2, MATRIX_3:def_4
.= width ((LineVec2Mx x2) * A) by A1, A2, A4, MATRIX_3:def_4 ;
A7: len (LineVec2Mx x1) = 1 by Def10;
then A8: 1 <= len ((LineVec2Mx x1) * A) by A2, A5, MATRIX_3:def_4;
A9: len (LineVec2Mx x2) = 1 by Def10;
thus (x1 + x2) * A = Line ((((LineVec2Mx x1) + (LineVec2Mx x2)) * A),1) by A1, Th50
.= Line ((((LineVec2Mx x1) * A) + ((LineVec2Mx x2) * A)),1) by A1, A2, A3, A5, A4, A7, A9, MATRIX_4:63
.= (x1 * A) + (x2 * A) by A6, A8, Th55 ; ::_thesis: verum
end;

theorem Th59: :: MATRIXR1:59
for a being Real
for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 holds
A * (a * x) = a * (A * x)
proof
let a be Real; ::_thesis: for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 holds
A * (a * x) = a * (A * x)
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st width A = len x & len x > 0 holds
A * (a * x) = a * (A * x)
let A be Matrix of REAL; ::_thesis: ( width A = len x & len x > 0 implies A * (a * x) = a * (A * x) )
assume that
A1: width A = len x and
A2: len x > 0 ; ::_thesis: A * (a * x) = a * (A * x)
A3: len (ColVec2Mx x) = len x by A2, Def9;
 width (ColVec2Mx x) = 1 by A2, Def9;
then A4: 1 <= width (A * (ColVec2Mx x)) by A1, A3, MATRIX_3:def_4;
thus A * (a * x) = Col ((A * (a * (ColVec2Mx x))),1) by A2, Th47
.= Col ((a * (A * (ColVec2Mx x))),1) by A1, A3, Th40
.= a * (A * x) by A4, Th56 ; ::_thesis: verum
end;

theorem :: MATRIXR1:60
for a being Real
for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds
(a * x) * A = a * (x * A)
proof
let a be Real; ::_thesis: for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds
(a * x) * A = a * (x * A)
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds
(a * x) * A = a * (x * A)
let A be Matrix of REAL; ::_thesis: ( len A = len x & len x > 0 & width A > 0 implies (a * x) * A = a * (x * A) )
assume that
A1: len A = len x and
A2: len x > 0 and
A3: width A > 0 ; ::_thesis: (a * x) * A = a * (x * A)
A4: (A @) * x = x * A by A1, A2, A3, Th52;
A5: width (A @) = len x by A1, A3, MATRIX_2:10;
then A6: (A @) * (a * x) = a * ((A @) * x) by A2, Th59;
A7: len (a * x) = len x by RVSUM_1:117;
 len (A @) > 0 by A3, MATRIX_2:10;
then  (a * x) * ((A @) @) = (A @) * (a * x) by A2, A5, A7, Th53;
hence  (a * x) * A = a * (x * A) by A1, A2, A3, A6, A4, MATRIX_2:13; ::_thesis: verum
end;

theorem Th61: :: MATRIXR1:61
for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 holds
len (A * x) = len A
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st width A = len x & len x > 0 holds
len (A * x) = len A
let A be Matrix of REAL; ::_thesis: ( width A = len x & len x > 0 implies len (A * x) = len A )
assume that
A1: width A = len x and
A2: len x > 0 ; ::_thesis: len (A * x) = len A
A3: len (ColVec2Mx x) = len x by A2, Def9;
len (Col ((A * (ColVec2Mx x)),1)) = len (A * (ColVec2Mx x)) by MATRIX_1:def_8
.= len A by A1, A3, MATRIX_3:def_4 ;
hence  len (A * x) = len A ; ::_thesis: verum
end;

theorem Th62: :: MATRIXR1:62
for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x holds
len (x * A) = width A
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A = len x holds
len (x * A) = width A
let A be Matrix of REAL; ::_thesis: ( len A = len x implies len (x * A) = width A )
assume A1: len A = len x ; ::_thesis: len (x * A) = width A
A2: width (LineVec2Mx x) = len x by Def10;
len (Line (((LineVec2Mx x) * A),1)) = width (MXF2MXR ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A))) by MATRIX_1:def_7
.= width A by A1, A2, MATRIX_3:def_4 ;
hence  len (x * A) = width A ; ::_thesis: verum
end;

theorem Th63: :: MATRIXR1:63
for x being FinSequence of REAL
for A, B being Matrix of REAL st len A = len B & width A = width B & width A = len x & len A > 0 & len x > 0 holds
(A + B) * x = (A * x) + (B * x)
proof
let x be FinSequence of REAL ; ::_thesis: for A, B being Matrix of REAL st len A = len B & width A = width B & width A = len x & len A > 0 & len x > 0 holds
(A + B) * x = (A * x) + (B * x)
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & width A = len x & len A > 0 & len x > 0 implies (A + B) * x = (A * x) + (B * x) )
assume that
A1: ( len A = len B & width A = width B ) and
A2: width A = len x and
A3: len A > 0 and
A4: len x > 0 ; ::_thesis: (A + B) * x = (A * x) + (B * x)
A5: len (ColVec2Mx x) = len x by A4, Def9;
then A6: len (A * (ColVec2Mx x)) = len A by A2, MATRIX_3:def_4
.= len (B * (ColVec2Mx x)) by A1, A2, A5, MATRIX_3:def_4 ;
A7: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A2, A5, MATRIX_3:def_4
.= 1 by A4, Def9 ;
thus (A + B) * x = Col (((A * (ColVec2Mx x)) + (B * (ColVec2Mx x))),1) by A1, A2, A3, A4, A5, MATRIX_4:63
.= (A * x) + (B * x) by A6, A7, Th54 ; ::_thesis: verum
end;

theorem Th64: :: MATRIXR1:64
for x being FinSequence of REAL
for A, B being Matrix of REAL st len A = len B & width A = width B & len A = len x & len x > 0 holds
x * (A + B) = (x * A) + (x * B)
proof
let x be FinSequence of REAL ; ::_thesis: for A, B being Matrix of REAL st len A = len B & width A = width B & len A = len x & len x > 0 holds
x * (A + B) = (x * A) + (x * B)
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & len A = len x & len x > 0 implies x * (A + B) = (x * A) + (x * B) )
assume that
A1: ( len A = len B & width A = width B ) and
A2: len A = len x and
A3: len x > 0 ; ::_thesis: x * (A + B) = (x * A) + (x * B)
A4: width (LineVec2Mx x) = len x by Def10;
then A5: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A2, MATRIX_3:def_4
.= 1 by Def10 ;
A6: width ((LineVec2Mx x) * A) = width A by A2, A4, MATRIX_3:def_4
.= width ((LineVec2Mx x) * B) by A1, A2, A4, MATRIX_3:def_4 ;
 len (LineVec2Mx x) = 1 by Def10;
hence x * (A + B) = Line ((((LineVec2Mx x) * A) + ((LineVec2Mx x) * B)),1) by A1, A2, A3, A4, MATRIX_4:62
.= (x * A) + (x * B) by A6, A5, Th55 ;
::_thesis: verum
end;

theorem :: MATRIXR1:65
for n, m being Element of NAT
for x being FinSequence of REAL st len x = m & n > 0 & m > 0 holds
(0_Rmatrix (n,m)) * x = 0* n
proof
let n, m be Element of NAT ; ::_thesis: for x being FinSequence of REAL st len x = m & n > 0 & m > 0 holds
(0_Rmatrix (n,m)) * x = 0* n
let x be FinSequence of REAL ; ::_thesis: ( len x = m & n > 0 & m > 0 implies (0_Rmatrix (n,m)) * x = 0* n )
assume that
A1: len x = m and
A2: n > 0 and
A3: m > 0 ; ::_thesis: (0_Rmatrix (n,m)) * x = 0* n
A4: width (0_Rmatrix (n,m)) = m by A2, MATRIX_1:23;
then A5: len ((0_Rmatrix (n,m)) * x) = len (0_Rmatrix (n,m)) by A1, A3, Th61;
A6: len (0_Rmatrix (n,m)) = n by A2, MATRIX_1:23;
then (0_Rmatrix (n,m)) * x = ((0_Rmatrix (n,m)) + (0_Rmatrix (n,m))) * x by A2, A4, Th36
.= ((0_Rmatrix (n,m)) * x) + ((0_Rmatrix (n,m)) * x) by A1, A2, A3, A6, A4, Th63 ;
then  0* n = (((0_Rmatrix (n,m)) * x) + ((0_Rmatrix (n,m)) * x)) - ((0_Rmatrix (n,m)) * x) by A6, A5, Th3;
hence  (0_Rmatrix (n,m)) * x = 0* n by A5, Th14; ::_thesis: verum
end;

theorem :: MATRIXR1:66
for n, m being Element of NAT
for x being FinSequence of REAL st len x = n & n > 0 holds
x * (0_Rmatrix (n,m)) = 0* m
proof
let n, m be Element of NAT ; ::_thesis: for x being FinSequence of REAL st len x = n & n > 0 holds
x * (0_Rmatrix (n,m)) = 0* m
let x be FinSequence of REAL ; ::_thesis: ( len x = n & n > 0 implies x * (0_Rmatrix (n,m)) = 0* m )
assume that
A1: len x = n and
A2: n > 0 ; ::_thesis: x * (0_Rmatrix (n,m)) = 0* m
A3: len (0_Rmatrix (n,m)) = n by A2, MATRIX_1:23;
then A4: len (x * (0_Rmatrix (n,m))) = width (0_Rmatrix (n,m)) by A1, Th62;
A5: width (0_Rmatrix (n,m)) = m by A2, MATRIX_1:23;
then x * (0_Rmatrix (n,m)) = x * ((0_Rmatrix (n,m)) + (0_Rmatrix (n,m))) by A2, A3, Th36
.= (x * (0_Rmatrix (n,m))) + (x * (0_Rmatrix (n,m))) by A1, A2, A5, A3, Th64 ;
then  0* m = ((x * (0_Rmatrix (n,m))) + (x * (0_Rmatrix (n,m)))) - (x * (0_Rmatrix (n,m))) by A5, A4, Th3;
hence  x * (0_Rmatrix (n,m)) = 0* m by A4, Th14; ::_thesis: verum
end;