:: MATRIX_5 semantic presentation

begin

theorem :: MATRIX_5:1
1 = 1_ F_Complex by COMPLEX1:def_4, COMPLFLD:8;

theorem :: MATRIX_5:2
0. F_Complex = 0 by COMPLFLD:7;

definition
let A be Matrix of COMPLEX;
func COMPLEX2Field A ->  Matrix of F_Complex equals :: MATRIX_5:def 1
A;
coherence
 A is Matrix of F_Complex by COMPLFLD:def_1;
end;

:: deftheorem  defines COMPLEX2Field MATRIX_5:def_1_:_
 for A being Matrix of COMPLEX holds COMPLEX2Field A = A;

definition
let A be Matrix of F_Complex;
func Field2COMPLEX A ->  Matrix of COMPLEX equals :: MATRIX_5:def 2
A;
coherence
 A is Matrix of COMPLEX by COMPLFLD:def_1;
end;

:: deftheorem  defines Field2COMPLEX MATRIX_5:def_2_:_
 for A being Matrix of F_Complex holds Field2COMPLEX A = A;

theorem :: MATRIX_5:3
for A, B being Matrix of COMPLEX st COMPLEX2Field A = COMPLEX2Field B holds
A = B ;

theorem :: MATRIX_5:4
for A, B being Matrix of F_Complex st Field2COMPLEX A = Field2COMPLEX B holds
A = B ;

theorem :: MATRIX_5:5
for A being Matrix of COMPLEX holds A = Field2COMPLEX (COMPLEX2Field A) ;

theorem :: MATRIX_5:6
for A being Matrix of F_Complex holds A = COMPLEX2Field (Field2COMPLEX A) ;

definition
let A, B be Matrix of COMPLEX;
funcA + B ->  Matrix of COMPLEX equals :: MATRIX_5:def 3
 Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B));
coherence
 Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B)) is Matrix of COMPLEX ;
end;

:: deftheorem  defines + MATRIX_5:def_3_:_
 for A, B being Matrix of COMPLEX holds A + B = Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B));

definition
let A be Matrix of COMPLEX;
func - A ->  Matrix of COMPLEX equals :: MATRIX_5:def 4
 Field2COMPLEX (- (COMPLEX2Field A));
coherence
 Field2COMPLEX (- (COMPLEX2Field A)) is Matrix of COMPLEX ;
end;

:: deftheorem  defines - MATRIX_5:def_4_:_
 for A being Matrix of COMPLEX holds - A = Field2COMPLEX (- (COMPLEX2Field A));

definition
let A, B be Matrix of COMPLEX;
funcA - B ->  Matrix of COMPLEX equals :: MATRIX_5:def 5
 Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B));
coherence
 Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B)) is Matrix of COMPLEX ;
funcA * B ->  Matrix of COMPLEX equals :: MATRIX_5:def 6
 Field2COMPLEX ((COMPLEX2Field A) * (COMPLEX2Field B));
coherence
 Field2COMPLEX ((COMPLEX2Field A) * (COMPLEX2Field B)) is Matrix of COMPLEX ;
end;

:: deftheorem  defines - MATRIX_5:def_5_:_
 for A, B being Matrix of COMPLEX holds A - B = Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B));

:: deftheorem  defines * MATRIX_5:def_6_:_
 for A, B being Matrix of COMPLEX holds A * B = Field2COMPLEX ((COMPLEX2Field A) * (COMPLEX2Field B));

definition
let x be complex number ;
let A be Matrix of COMPLEX;
funcx * A ->  Matrix of COMPLEX means :Def7: :: MATRIX_5:def 7
 for ea being Element of F_Complex st ea = x holds
it = Field2COMPLEX (ea * (COMPLEX2Field A));
existence
 ex b1 being Matrix of COMPLEX st
for ea being Element of F_Complex st ea = x holds
b1 = Field2COMPLEX (ea * (COMPLEX2Field A))
proof
 x in COMPLEX by XCMPLX_0:def_2;
then reconsider aa = x as Element of F_Complex by COMPLFLD:def_1;
set C = Field2COMPLEX (aa * (COMPLEX2Field A));
 for ea being Element of F_Complex st ea = x holds
Field2COMPLEX (aa * (COMPLEX2Field A)) = Field2COMPLEX (ea * (COMPLEX2Field A)) ;
hence  ex b1 being Matrix of COMPLEX st
for ea being Element of F_Complex st ea = x holds
b1 = Field2COMPLEX (ea * (COMPLEX2Field A)) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Matrix of COMPLEX st ( for ea being Element of F_Complex st ea = x holds
b1 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) & ( for ea being Element of F_Complex st ea = x holds
b2 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) holds
b1 = b2
proof
 x in COMPLEX by XCMPLX_0:def_2;
then reconsider aa = x as Element of F_Complex by COMPLFLD:def_1;
let C1, C2 be Matrix of COMPLEX; ::_thesis: ( ( for ea being Element of F_Complex st ea = x holds
C1 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) & ( for ea being Element of F_Complex st ea = x holds
C2 = Field2COMPLEX (ea * (COMPLEX2Field A)) ) implies C1 = C2 )
assume that
A1: for ea being Element of F_Complex st ea = x holds
C1 = Field2COMPLEX (ea * (COMPLEX2Field A)) and
A2: for ea being Element of F_Complex st ea = x holds
C2 = Field2COMPLEX (ea * (COMPLEX2Field A)) ; ::_thesis: C1 = C2
 C2 = Field2COMPLEX (aa * (COMPLEX2Field A)) by A2;
hence  C1 = C2 by A1; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines * MATRIX_5:def_7_:_
 for x being complex number
for A, b3 being Matrix of COMPLEX holds
( b3 = x * A iff for ea being Element of F_Complex st ea = x holds
b3 = Field2COMPLEX (ea * (COMPLEX2Field A)) );

theorem :: MATRIX_5:7
for A being Matrix of COMPLEX holds
( len A = len (COMPLEX2Field A) & width A = width (COMPLEX2Field A) ) ;

theorem :: MATRIX_5:8
for A being Matrix of F_Complex holds
( len A = len (Field2COMPLEX A) & width A = width (Field2COMPLEX A) ) ;

theorem Th9: :: MATRIX_5:9
for K being Field
for M being Matrix of K holds (1_ K) * M = M
proof
let K be Field; ::_thesis: for M being Matrix of K holds (1_ K) * M = M
let M be Matrix of K; ::_thesis: (1_ K) * M = M
A1: for i, j being Nat st [i,j] in Indices M holds
((1_ K) * M) * (i,j) = M * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M implies ((1_ K) * M) * (i,j) = M * (i,j) )
A2: (1_ K) * (M * (i,j)) = M * (i,j) by VECTSP_1:def_8;
assume  [i,j] in Indices M ; ::_thesis: ((1_ K) * M) * (i,j) = M * (i,j)
hence  ((1_ K) * M) * (i,j) = M * (i,j) by A2, MATRIX_3:def_5; ::_thesis: verum
end;
 ( len ((1_ K) * M) = len M & width ((1_ K) * M) = width M ) by MATRIX_3:def_5;
hence  (1_ K) * M = M by A1, MATRIX_1:21; ::_thesis: verum
end;

theorem :: MATRIX_5:10
for M being Matrix of COMPLEX holds 1 * M = M
proof
set e = 1_ F_Complex;
let M be Matrix of COMPLEX; ::_thesis: 1 * M = M
 1 * M = Field2COMPLEX ((1_ F_Complex) * (COMPLEX2Field M)) by Def7, COMPLEX1:def_4, COMPLFLD:8;
hence  1 * M = M by Th9; ::_thesis: verum
end;

theorem :: MATRIX_5:11
for K being Field
for a, b being Element of K
for M being Matrix of K holds a * (b * M) = (a * b) * M
proof
let K be Field; ::_thesis: for a, b being Element of K
for M being Matrix of K holds a * (b * M) = (a * b) * M
let a, b be Element of K; ::_thesis: for M being Matrix of K holds a * (b * M) = (a * b) * M
let M be Matrix of K; ::_thesis: a * (b * M) = (a * b) * M
A1: ( len ((a * b) * M) = len M & width ((a * b) * M) = width M ) by MATRIX_3:def_5;
A2: len (a * (b * M)) = len (b * M) by MATRIX_3:def_5;
A3: width (a * (b * M)) = width (b * M) by MATRIX_3:def_5;
then A4: width (a * (b * M)) = width M by MATRIX_3:def_5;
A5: ( len (b * M) = len M & width (b * M) = width M ) by MATRIX_3:def_5;
A6: for i, j being Nat st [i,j] in Indices (a * (b * M)) holds
(a * (b * M)) * (i,j) = ((a * b) * M) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * (b * M)) implies (a * (b * M)) * (i,j) = ((a * b) * M) * (i,j) )
assume A7: [i,j] in Indices (a * (b * M)) ; ::_thesis: (a * (b * M)) * (i,j) = ((a * b) * M) * (i,j)
A8: Indices (b * M) = Indices M by A5, MATRIX_4:55;
A9: Indices (a * (b * M)) = Indices (b * M) by A2, A3, MATRIX_4:55;
then (a * (b * M)) * (i,j) = a * ((b * M) * (i,j)) by A7, MATRIX_3:def_5
.= a * (b * (M * (i,j))) by A7, A9, A8, MATRIX_3:def_5
.= (a * b) * (M * (i,j)) by GROUP_1:def_3 ;
hence  (a * (b * M)) * (i,j) = ((a * b) * M) * (i,j) by A7, A9, A8, MATRIX_3:def_5; ::_thesis: verum
end;
 len (a * (b * M)) = len M by A2, MATRIX_3:def_5;
hence  a * (b * M) = (a * b) * M by A1, A4, A6, MATRIX_1:21; ::_thesis: verum
end;

theorem Th12: :: MATRIX_5:12
for K being Field
for a, b being Element of K
for M being Matrix of K holds (a + b) * M = (a * M) + (b * M)
proof
let K be Field; ::_thesis: for a, b being Element of K
for M being Matrix of K holds (a + b) * M = (a * M) + (b * M)
let a, b be Element of K; ::_thesis: for M being Matrix of K holds (a + b) * M = (a * M) + (b * M)
let M be Matrix of K; ::_thesis: (a + b) * M = (a * M) + (b * M)
A1: ( len (a * M) = len M & width (a * M) = width M ) by MATRIX_3:def_5;
A2: ( len ((a + b) * M) = len M & width ((a + b) * M) = width M ) by MATRIX_3:def_5;
A3: for i, j being Nat st [i,j] in Indices ((a + b) * M) holds
((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((a + b) * M) implies ((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j) )
assume A4: [i,j] in Indices ((a + b) * M) ; ::_thesis: ((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j)
A5: Indices ((a + b) * M) = Indices M by A2, MATRIX_4:55;
 Indices (a * M) = Indices M by A1, MATRIX_4:55;
then ((a * M) + (b * M)) * (i,j) = ((a * M) * (i,j)) + ((b * M) * (i,j)) by A4, A5, MATRIX_3:def_3
.= (a * (M * (i,j))) + ((b * M) * (i,j)) by A4, A5, MATRIX_3:def_5
.= (a * (M * (i,j))) + (b * (M * (i,j))) by A4, A5, MATRIX_3:def_5
.= (a + b) * (M * (i,j)) by VECTSP_1:def_7 ;
hence  ((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j) by A4, A5, MATRIX_3:def_5; ::_thesis: verum
end;
 ( len ((a * M) + (b * M)) = len (a * M) & width ((a * M) + (b * M)) = width (a * M) ) by MATRIX_3:def_3;
hence  (a + b) * M = (a * M) + (b * M) by A2, A1, A3, MATRIX_1:21; ::_thesis: verum
end;

theorem :: MATRIX_5:13
for M being Matrix of COMPLEX holds M + M = 2 * M
proof
reconsider e2 = (1_ F_Complex) + (1_ F_Complex) as Element of F_Complex ;
let M be Matrix of COMPLEX; ::_thesis: M + M = 2 * M
A1: (1_ F_Complex) * (COMPLEX2Field M) = COMPLEX2Field M by Th9;
2 * M = Field2COMPLEX (e2 * (COMPLEX2Field M)) by Def7, COMPLEX1:def_4, COMPLFLD:8
.= Field2COMPLEX ((COMPLEX2Field M) + (COMPLEX2Field M)) by A1, Th12 ;
hence  M + M = 2 * M ; ::_thesis: verum
end;

theorem :: MATRIX_5:14
for M being Matrix of COMPLEX holds (M + M) + M = 3 * M
proof
reconsider rr = 1 + 1 as Element of COMPLEX by XCMPLX_0:def_2;
reconsider e3 = ((1_ F_Complex) + (1_ F_Complex)) + (1_ F_Complex) as Element of F_Complex ;
let M be Matrix of COMPLEX; ::_thesis: (M + M) + M = 3 * M
A1: ( len M = len (COMPLEX2Field M) & width M = width (COMPLEX2Field M) ) ;
A2: (1_ F_Complex) + (1_ F_Complex) = the addF of F_Complex . ((1_ F_Complex),(1_ F_Complex)) by RLVECT_1:2
.= addcomplex . (1r,1r) by COMPLFLD:8, COMPLFLD:def_1
.= 1 + 1 by BINOP_2:def_3, COMPLEX1:def_4 ;
((1_ F_Complex) + (1_ F_Complex)) + (1_ F_Complex) = the addF of F_Complex . (((1_ F_Complex) + (1_ F_Complex)),(1_ F_Complex)) by RLVECT_1:2
.= addcomplex . ((1 + 1),1) by A2, COMPLFLD:def_1
.= rr + 1 by BINOP_2:def_3
.= 3 ;
then 3 * M = Field2COMPLEX (e3 * (COMPLEX2Field M)) by Def7
.= Field2COMPLEX (((1_ F_Complex) * (COMPLEX2Field M)) + (((1_ F_Complex) + (1_ F_Complex)) * (COMPLEX2Field M))) by Th12
.= Field2COMPLEX ((COMPLEX2Field M) + (((1_ F_Complex) + (1_ F_Complex)) * (COMPLEX2Field M))) by Th9
.= Field2COMPLEX ((COMPLEX2Field M) + (((1_ F_Complex) * (COMPLEX2Field M)) + ((1_ F_Complex) * (COMPLEX2Field M)))) by Th12
.= Field2COMPLEX ((COMPLEX2Field M) + ((COMPLEX2Field M) + ((1_ F_Complex) * (COMPLEX2Field M)))) by Th9
.= Field2COMPLEX ((COMPLEX2Field M) + ((COMPLEX2Field M) + (COMPLEX2Field M))) by Th9
.= Field2COMPLEX (((COMPLEX2Field M) + (COMPLEX2Field M)) + (COMPLEX2Field M)) by A1, MATRIX_3:3 ;
hence  (M + M) + M = 3 * M ; ::_thesis: verum
end;

definition
let n, m be Nat;
func 0_Cx (n,m) ->  Matrix of COMPLEX equals :: MATRIX_5:def 8
 Field2COMPLEX (0. (F_Complex,n,m));
coherence
 Field2COMPLEX (0. (F_Complex,n,m)) is Matrix of COMPLEX ;
end;

:: deftheorem  defines 0_Cx MATRIX_5:def_8_:_
 for n, m being Nat holds 0_Cx (n,m) = Field2COMPLEX (0. (F_Complex,n,m));

theorem :: MATRIX_5:15
for n, m being Element of NAT holds COMPLEX2Field (0_Cx (n,m)) = 0. (F_Complex,n,m) ;

theorem :: MATRIX_5:16
for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & M1 = M1 + M2 holds
M2 = 0_Cx ((len M1),(width M1))
proof
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & M1 = M1 + M2 implies M2 = 0_Cx ((len M1),(width M1)) )
assume that
A1: ( len M1 = len M2 & width M1 = width M2 ) and
A2: M1 = M1 + M2 ; ::_thesis: M2 = 0_Cx ((len M1),(width M1))
0_Cx ((len M1),(width M1)) = (M1 + M2) + (- M1) by A2, MATRIX_4:2
.= Field2COMPLEX (((COMPLEX2Field M2) + (COMPLEX2Field M1)) - (COMPLEX2Field M1)) by A1, MATRIX_3:2
.= M2 by A1, MATRIX_4:21 ;
hence  M2 = 0_Cx ((len M1),(width M1)) ; ::_thesis: verum
end;

theorem :: MATRIX_5:17
for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & M1 + M2 = 0_Cx ((len M1),(width M1)) holds
M2 = - M1
proof
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & M1 + M2 = 0_Cx ((len M1),(width M1)) implies M2 = - M1 )
assume that
A1: ( len M1 = len M2 & width M1 = width M2 ) and
A2: M1 + M2 = 0_Cx ((len M1),(width M1)) ; ::_thesis: M2 = - M1
A3: ( len (- M2) = len M2 & width (- M2) = width M2 ) by MATRIX_3:def_2;
 COMPLEX2Field (0_Cx ((len M1),(width M1))) = (COMPLEX2Field M1) - (- (COMPLEX2Field M2)) by A2, MATRIX_4:1;
then  COMPLEX2Field M1 = - (COMPLEX2Field M2) by A1, A3, MATRIX_4:7;
hence  M2 = - M1 by MATRIX_4:1; ::_thesis: verum
end;

theorem :: MATRIX_5:18
for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & M2 - M1 = M2 holds
M1 = 0_Cx ((len M1),(width M1))
proof
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & M2 - M1 = M2 implies M1 = 0_Cx ((len M1),(width M1)) )
assume that
A1: ( len M1 = len M2 & width M1 = width M2 ) and
A2: M2 - M1 = M2 ; ::_thesis: M1 = 0_Cx ((len M1),(width M1))
 (COMPLEX2Field M2) + (COMPLEX2Field M1) = COMPLEX2Field M2 by A1, A2, MATRIX_4:22;
hence  M1 = 0_Cx ((len M1),(width M1)) by A1, MATRIX_4:6; ::_thesis: verum
end;

theorem :: MATRIX_5:19
for M being Matrix of COMPLEX holds M + (0_Cx ((len M),(width M))) = M
proof
let M be Matrix of COMPLEX; ::_thesis: M + (0_Cx ((len M),(width M))) = M
A1: ( len M = len (COMPLEX2Field M) & width M = width (COMPLEX2Field M) ) ;
M + (0_Cx ((len M),(width M))) = M + (- (0_Cx ((len M),(width M)))) by MATRIX_4:9
.= Field2COMPLEX ((COMPLEX2Field M) - ((COMPLEX2Field M) - (COMPLEX2Field M))) by MATRIX_4:3
.= M by A1, MATRIX_4:11 ;
hence  M + (0_Cx ((len M),(width M))) = M ; ::_thesis: verum
end;

theorem Th20: :: MATRIX_5:20
for K being Field
for b being Element of K
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
b * (M1 + M2) = (b * M1) + (b * M2)
proof
let K be Field; ::_thesis: for b being Element of K
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
b * (M1 + M2) = (b * M1) + (b * M2)
let b be Element of K; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
b * (M1 + M2) = (b * M1) + (b * M2)
let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies b * (M1 + M2) = (b * M1) + (b * M2) )
A1: ( len (b * (M1 + M2)) = len (M1 + M2) & width (b * (M1 + M2)) = width (M1 + M2) ) by MATRIX_3:def_5;
A2: ( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 ) by MATRIX_3:def_3;
A3: ( len (b * M1) = len M1 & width (b * M1) = width M1 ) by MATRIX_3:def_5;
assume A4: ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: b * (M1 + M2) = (b * M1) + (b * M2)
A5: for i, j being Nat st [i,j] in Indices (b * (M1 + M2)) holds
(b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (b * (M1 + M2)) implies (b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j) )
assume A6: [i,j] in Indices (b * (M1 + M2)) ; ::_thesis: (b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j)
A7: Indices M2 = Indices M1 by A4, MATRIX_4:55;
A8: Indices (b * (M1 + M2)) = Indices (M1 + M2) by A1, MATRIX_4:55;
A9: Indices (M1 + M2) = Indices M1 by A2, MATRIX_4:55;
 Indices (b * M1) = Indices M1 by A3, MATRIX_4:55;
then ((b * M1) + (b * M2)) * (i,j) = ((b * M1) * (i,j)) + ((b * M2) * (i,j)) by A6, A8, A9, MATRIX_3:def_3
.= (b * (M1 * (i,j))) + ((b * M2) * (i,j)) by A6, A8, A9, MATRIX_3:def_5
.= (b * (M1 * (i,j))) + (b * (M2 * (i,j))) by A6, A8, A9, A7, MATRIX_3:def_5
.= b * ((M1 * (i,j)) + (M2 * (i,j))) by VECTSP_1:def_7 ;
then ((b * M1) + (b * M2)) * (i,j) = b * ((M1 + M2) * (i,j)) by A6, A8, A9, MATRIX_3:def_3
.= (b * (M1 + M2)) * (i,j) by A6, A8, MATRIX_3:def_5 ;
hence  (b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j) ; ::_thesis: verum
end;
 ( len ((b * M1) + (b * M2)) = len (b * M1) & width ((b * M1) + (b * M2)) = width (b * M1) ) by MATRIX_3:def_3;
hence  b * (M1 + M2) = (b * M1) + (b * M2) by A1, A2, A3, A5, MATRIX_1:21; ::_thesis: verum
end;

theorem :: MATRIX_5:21
for M1, M2 being Matrix of COMPLEX
for a being complex number st len M1 = len M2 & width M1 = width M2 holds
a * (M1 + M2) = (a * M1) + (a * M2)
proof
let M1, M2 be Matrix of COMPLEX; ::_thesis: for a being complex number st len M1 = len M2 & width M1 = width M2 holds
a * (M1 + M2) = (a * M1) + (a * M2)
let a be complex number ; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies a * (M1 + M2) = (a * M1) + (a * M2) )
assume A1: ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: a * (M1 + M2) = (a * M1) + (a * M2)
 a in COMPLEX by XCMPLX_0:def_2;
then reconsider ea = a as Element of F_Complex by COMPLFLD:def_1;
A2: (a * M1) + (a * M2) = Field2COMPLEX ((COMPLEX2Field (Field2COMPLEX (ea * (COMPLEX2Field M1)))) + (COMPLEX2Field (a * M2))) by Def7
.= Field2COMPLEX ((ea * (COMPLEX2Field M1)) + (COMPLEX2Field (Field2COMPLEX (ea * (COMPLEX2Field M2))))) by Def7
.= Field2COMPLEX ((ea * (COMPLEX2Field M1)) + (ea * (COMPLEX2Field M2))) ;
a * (M1 + M2) = Field2COMPLEX (ea * (COMPLEX2Field (M1 + M2))) by Def7
.= Field2COMPLEX ((ea * (COMPLEX2Field M1)) + (ea * (COMPLEX2Field M2))) by A1, Th20 ;
hence  a * (M1 + M2) = (a * M1) + (a * M2) by A2; ::_thesis: verum
end;

theorem Th22: :: MATRIX_5:22
for K being Field
for M1, M2 being Matrix of K st width M1 = len M2 & len M1 > 0 & len M2 > 0 holds
(0. (K,(len M1),(width M1))) * M2 = 0. (K,(len M1),(width M2))
proof
let K be Field; ::_thesis: for M1, M2 being Matrix of K st width M1 = len M2 & len M1 > 0 & len M2 > 0 holds
(0. (K,(len M1),(width M1))) * M2 = 0. (K,(len M1),(width M2))
let M1, M2 be Matrix of K; ::_thesis: ( width M1 = len M2 & len M1 > 0 & len M2 > 0 implies (0. (K,(len M1),(width M1))) * M2 = 0. (K,(len M1),(width M2)) )
assume that
A1: width M1 = len M2 and
A2: len M1 > 0 and
A3: len M2 > 0 ; ::_thesis: (0. (K,(len M1),(width M1))) * M2 = 0. (K,(len M1),(width M2))
A4: len (0. (K,(len M1),(width M1))) = len M1 by MATRIX_1:def_2;
then A5: width (0. (K,(len M1),(width M1))) = width M1 by A2, MATRIX_1:20;
then A6: len ((0. (K,(len M1),(width M1))) * M2) = len (0. (K,(len M1),(width M1))) by A1, MATRIX_3:def_4;
A7: width ((0. (K,(len M1),(width M1))) * M2) = width M2 by A1, A5, MATRIX_3:def_4;
set B = (0. (K,(len M1),(width M1))) * M2;
A8: width (- ((0. (K,(len M1),(width M1))) * M2)) = width ((0. (K,(len M1),(width M1))) * M2) by MATRIX_3:def_2;
(0. (K,(len M1),(width M1))) * M2 = ((0. (K,(len M1),(width M1))) + (0. (K,(len M1),(width M1)))) * M2 by MATRIX_3:4
.= ((0. (K,(len M1),(width M1))) * M2) + ((0. (K,(len M1),(width M1))) * M2) by A1, A2, A3, A4, A5, MATRIX_4:63 ;
then  ( len (- ((0. (K,(len M1),(width M1))) * M2)) = len ((0. (K,(len M1),(width M1))) * M2) & 0. (K,(len M1),(width M2)) = (((0. (K,(len M1),(width M1))) * M2) + ((0. (K,(len M1),(width M1))) * M2)) + (- ((0. (K,(len M1),(width M1))) * M2)) ) by A4, A6, A7, MATRIX_3:def_2, MATRIX_4:2;
then  0. (K,(len M1),(width M2)) = ((0. (K,(len M1),(width M1))) * M2) + (((0. (K,(len M1),(width M1))) * M2) - ((0. (K,(len M1),(width M1))) * M2)) by A8, MATRIX_3:3
.= (0. (K,(len M1),(width M1))) * M2 by A6, A8, MATRIX_4:20 ;
hence  (0. (K,(len M1),(width M1))) * M2 = 0. (K,(len M1),(width M2)) ; ::_thesis: verum
end;

theorem :: MATRIX_5:23
for M1, M2 being Matrix of COMPLEX st width M1 = len M2 & len M1 > 0 & len M2 > 0 holds
(0_Cx ((len M1),(width M1))) * M2 = 0_Cx ((len M1),(width M2))
proof
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( width M1 = len M2 & len M1 > 0 & len M2 > 0 implies (0_Cx ((len M1),(width M1))) * M2 = 0_Cx ((len M1),(width M2)) )
A1: len M1 = len (COMPLEX2Field M1) ;
assume  ( width M1 = len M2 & len M1 > 0 & len M2 > 0 ) ; ::_thesis: (0_Cx ((len M1),(width M1))) * M2 = 0_Cx ((len M1),(width M2))
hence  (0_Cx ((len M1),(width M1))) * M2 = 0_Cx ((len M1),(width M2)) by A1, Th22; ::_thesis: verum
end;

theorem Th24: :: MATRIX_5:24
for K being Field
for M1 being Matrix of K st len M1 > 0 holds
(0. K) * M1 = 0. (K,(len M1),(width M1))
proof
let K be Field; ::_thesis: for M1 being Matrix of K st len M1 > 0 holds
(0. K) * M1 = 0. (K,(len M1),(width M1))
let M1 be Matrix of K; ::_thesis: ( len M1 > 0 implies (0. K) * M1 = 0. (K,(len M1),(width M1)) )
A1: len (0. (K,(len M1),(width M1))) = len M1 by MATRIX_1:def_2;
assume  len M1 > 0 ; ::_thesis: (0. K) * M1 = 0. (K,(len M1),(width M1))
then A2: width (0. (K,(len M1),(width M1))) = width M1 by A1, MATRIX_1:20;
A3: for i, j being Nat st [i,j] in Indices (0. (K,(len M1),(width M1))) holds
((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (0. (K,(len M1),(width M1))) implies ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j) )
assume A4: [i,j] in Indices (0. (K,(len M1),(width M1))) ; ::_thesis: ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j)
 Indices (0. (K,(len M1),(width M1))) = Indices M1 by A1, A2, MATRIX_4:55;
then A5: ((0. K) * M1) * (i,j) = (0. K) * (M1 * (i,j)) by A4, MATRIX_3:def_5;
 (0. (K,(len M1),(width M1))) * (i,j) = 0. K by A4, MATRIX_3:1;
hence  ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j) by A5, VECTSP_1:6; ::_thesis: verum
end;
 ( len ((0. K) * M1) = len M1 & width ((0. K) * M1) = width M1 ) by MATRIX_3:def_5;
hence  (0. K) * M1 = 0. (K,(len M1),(width M1)) by A1, A2, A3, MATRIX_1:21; ::_thesis: verum
end;

theorem :: MATRIX_5:25
for M1 being Matrix of COMPLEX st len M1 > 0 holds
0 * M1 = 0_Cx ((len M1),(width M1))
proof
reconsider ea = 0 as Element of F_Complex by COMPLFLD:def_1;
let M1 be Matrix of COMPLEX; ::_thesis: ( len M1 > 0 implies 0 * M1 = 0_Cx ((len M1),(width M1)) )
assume A1: len M1 > 0 ; ::_thesis: 0 * M1 = 0_Cx ((len M1),(width M1))
0 * M1 = Field2COMPLEX (ea * (COMPLEX2Field M1)) by Def7
.= 0_Cx ((len M1),(width M1)) by A1, Th24, COMPLFLD:7 ;
hence  0 * M1 = 0_Cx ((len M1),(width M1)) ; ::_thesis: verum
end;

definition
let s be complex-valued Function;
let k be set ;
:: original: .
redefine funcs . k ->  Element of COMPLEX ;
coherence
 s . k is Element of COMPLEX
proof
percases ( k in dom s or not k in dom s ) ;
supposeA1: k in dom s ; ::_thesis: s . k is Element of COMPLEX
A2: rng s c= COMPLEX by VALUED_0:def_1;
 s . k in rng s by A1, FUNCT_1:def_3;
hence  s . k is Element of COMPLEX by A2; ::_thesis: verum
end;
suppose not k in dom s ; ::_thesis: s . k is Element of COMPLEX
then  s . k = 0c by FUNCT_1:def_2;
hence  s . k is Element of COMPLEX ; ::_thesis: verum
end;
end;
end;
end;

theorem :: MATRIX_5:26
for i, j being Element of NAT
for M1, M2 being Matrix of COMPLEX st len M2 > 0 holds
ex s being FinSequence of COMPLEX st
( len s = len M2 & s . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < len M2 holds
s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) )
proof
let i, j be Element of NAT ; ::_thesis: for M1, M2 being Matrix of COMPLEX st len M2 > 0 holds
ex s being FinSequence of COMPLEX st
( len s = len M2 & s . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < len M2 holds
s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) )
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M2 > 0 implies ex s being FinSequence of COMPLEX st
( len s = len M2 & s . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < len M2 holds
s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) )
defpred S1[ Element of NAT ] means  ex q being FinSequence of COMPLEX st
( 1 <= $1 + 1 & $1 + 1 <= len M2 implies ( len q = $1 + 1 & q . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < $1 + 1 holds
q . (k + 1) = (q . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) );
set q0 = <*((M1 * (i,1)) * (M2 * (1,j)))*>;
A1: for k being Element of NAT st 1 <= k & k < 1 holds
<*((M1 * (i,1)) * (M2 * (1,j)))*> . (k + 1) = (<*((M1 * (i,1)) * (M2 * (1,j)))*> . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ;
A2: for i2 being Element of NAT st S1[i2] holds
S1[i2 + 1]
proof
let i2 be Element of NAT ; ::_thesis: ( S1[i2] implies S1[i2 + 1] )
set k0 = i2;
assume  S1[i2] ; ::_thesis: S1[i2 + 1]
then consider q2 being FinSequence of COMPLEX  such that
A3: ( 1 <= i2 + 1 & i2 + 1 <= len M2 implies ( len q2 = i2 + 1 & q2 . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k2 being Element of NAT st 1 <= k2 & k2 < i2 + 1 holds
q2 . (k2 + 1) = (q2 . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) ) ) ) ;
set q3 = q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>;
 ( 1 <= (i2 + 1) + 1 & (i2 + 1) + 1 <= len M2 implies ( len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) = (i2 + 1) + 1 & (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < (i2 + 1) + 1 holds
(q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) )
proof
assume that
 1 <= (i2 + 1) + 1 and
A4: (i2 + 1) + 1 <= len M2 ; ::_thesis: ( len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) = (i2 + 1) + 1 & (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < (i2 + 1) + 1 holds
(q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) )
percases 1 <= i2 + 1 by NAT_1:12;
supposeA5: 1 <= i2 + 1 ; ::_thesis: ( len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) = (i2 + 1) + 1 & (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < (i2 + 1) + 1 holds
(q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) )
A6: len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) = (len q2) + (len <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by FINSEQ_1:22
.= (i2 + 1) + 1 by A3, A4, A5, FINSEQ_1:39, NAT_1:13 ;
A7: for k2 being Element of NAT st 1 <= k2 & k2 < (i2 + 1) + 1 holds
(q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j)))
proof
let k2 be Element of NAT ; ::_thesis: ( 1 <= k2 & k2 < (i2 + 1) + 1 implies (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) )
assume that
A8: 1 <= k2 and
A9: k2 < (i2 + 1) + 1 ; ::_thesis: (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j)))
A10: k2 <= i2 + 1 by A9, NAT_1:13;
percases ( k2 < i2 + 1 or k2 = i2 + 1 ) by A10, XXREAL_0:1;
supposeA11: k2 < i2 + 1 ; ::_thesis: (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j)))
then  k2 < len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by A6, NAT_1:13;
then  k2 < (len q2) + (len <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by FINSEQ_1:22;
then  k2 < (len q2) + 1 by FINSEQ_1:39;
then  k2 <= len q2 by NAT_1:13;
then  k2 in dom q2 by A8, FINSEQ_3:25;
then A12: (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2 = q2 . k2 by FINSEQ_1:def_7;
 k2 + 1 < (i2 + 1) + 1 by A11, XREAL_1:6;
then  k2 + 1 < (len q2) + (len <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by A6, FINSEQ_1:22;
then  k2 + 1 < (len q2) + 1 by FINSEQ_1:39;
then A13: k2 + 1 <= len q2 by NAT_1:13;
 1 <= k2 + 1 by A8, NAT_1:13;
then  k2 + 1 in dom q2 by A13, FINSEQ_3:25;
then  (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = q2 . (k2 + 1) by FINSEQ_1:def_7;
hence  (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) by A3, A4, A5, A8, A11, A12, NAT_1:13; ::_thesis: verum
end;
supposeA14: k2 = i2 + 1 ; ::_thesis: (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j)))
then  k2 < (i2 + 1) + 1 by NAT_1:13;
then  k2 < (len q2) + (len <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by A6, FINSEQ_1:22;
then  k2 < (len q2) + 1 by FINSEQ_1:39;
then  k2 <= len q2 by NAT_1:13;
then  k2 in dom q2 by A8, FINSEQ_3:25;
then A15: (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2 = q2 . k2 by FINSEQ_1:def_7;
 1 in Seg 1 by FINSEQ_1:3;
then  ( <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*> . 1 = (q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))) & 1 in dom <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*> ) by FINSEQ_1:def_8;
hence  (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k2 + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) by A3, A4, A5, A14, A15, FINSEQ_1:def_7, NAT_1:13; ::_thesis: verum
end;
end;
end;
 1 < len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by A5, A6, NAT_1:13;
then  1 < (len q2) + (len <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) by FINSEQ_1:22;
then  1 < (len q2) + 1 by FINSEQ_1:39;
then  1 <= len q2 by NAT_1:13;
then  1 in dom q2 by FINSEQ_3:25;
hence  ( len (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) = (i2 + 1) + 1 & (q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < (i2 + 1) + 1 holds
(q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . (k + 1) = ((q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) by A3, A4, A5, A6, A7, FINSEQ_1:def_7, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence  S1[i2 + 1] ; ::_thesis: verum
end;
 ( len <*((M1 * (i,1)) * (M2 * (1,j)))*> = 1 & <*((M1 * (i,1)) * (M2 * (1,j)))*> . 1 = (M1 * (i,1)) * (M2 * (1,j)) ) by FINSEQ_1:39, FINSEQ_1:def_8;
then A16: S1[ 0 ] by A1;
A17: for j being Element of NAT holds S1[j] from NAT_1:sch_1(A16, A2);
assume A18: len M2 > 0 ; ::_thesis: ex s being FinSequence of COMPLEX st
( len s = len M2 & s . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < len M2 holds
s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) )
then  0 + 1 <= len M2 by NAT_1:8;
then  (0 + 1) - 1 <= (len M2) - 1 by XREAL_1:9;
then A19: (len M2) -' 1 = (len M2) - 1 by XREAL_0:def_2;
then  0 + 1 <= ((len M2) -' 1) + 1 by A18, NAT_1:8;
hence  ex s being FinSequence of COMPLEX st
( len s = len M2 & s . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Element of NAT st 1 <= k & k < len M2 holds
s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) by A19, A17; ::_thesis: verum
end;