let i, j be 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 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 Nat st 1 <= k & k < len M2 holds
s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) )
defpred S₁[ 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 Nat st 1 <= k & k < $1 + 1 holds
q . (k + 1) = (q . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) );
reconsider q0 = <*((M1 * (i,1)) * (M2 * (1,j)))*> as FinSequence of COMPLEX by RVSUM_1:146;
A1: for k being Nat st 1 <= k & k < 1 holds
q0 . (k + 1) = (q0 . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ;
A2: for i2 being Nat st S₁[i2] holds
S₁[i2 + 1]

proof

let i2 be Nat; :: thesis: ( S₁[i2] implies S₁[i2 + 1] )
set k0 = i2;
assume S₁[i2] ; :: thesis: S₁[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 Nat st 1 <= k2 & k2 < i2 + 1 holds
q2 . (k2 + 1) = (q2 . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) ) ) ) ;
reconsider q3 = q2 ^ <*((q2 . (i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*> as FinSequence of COMPLEX by RVSUM_1:146;
( 1 <= (i2 + 1) + 1 & (i2 + 1) + 1 <= len M2 implies ( len q3 = (i2 + 1) + 1 & q3 . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Nat st 1 <= k & k < (i2 + 1) + 1 holds
q3 . (k + 1) = (q3 . 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 q3 = (i2 + 1) + 1 & q3 . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Nat st 1 <= k & k < (i2 + 1) + 1 holds
q3 . (k + 1) = (q3 . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) )
A5: 1 <= i2 + 1 by NAT_1:12;
thus A6: len q3 = (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 ; :: thesis: ( q3 . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Nat st 1 <= k & k < (i2 + 1) + 1 holds
q3 . (k + 1) = (q3 . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) )
A7: for k2 being Nat st 1 <= k2 & k2 < (i2 + 1) + 1 holds
q3 . (k2 + 1) = (q3 . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j)))

proof

let k2 be Nat; :: thesis: ( 1 <= k2 & k2 < (i2 + 1) + 1 implies q3 . (k2 + 1) = (q3 . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) )
assume that
A8: 1 <= k2 and
A9: k2 < (i2 + 1) + 1 ; :: thesis: q3 . (k2 + 1) = (q3 . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j)))
A10: k2 <= i2 + 1 by A9, NAT_1:13;

per cases ( k2 < i2 + 1 or k2 = i2 + 1 ) by A10, XXREAL_0:1;

suppose A11: k2 < i2 + 1 ; :: thesis: q3 . (k2 + 1) = (q3 . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j)))

then k2 < len q3 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: q3 . 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 q3 . (k2 + 1) = q2 . (k2 + 1) by FINSEQ_1:def 7;
hence q3 . (k2 + 1) = (q3 . k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) by A3, A4, A5, A8, A11, A12, NAT_1:13; :: thesis: verum

end;

suppose A14: k2 = i2 + 1 ; :: thesis: q3 . (k2 + 1) = (q3 . 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: q3 . 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 q3 . (k2 + 1) = (q3 . 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 ( q3 . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Nat st 1 <= k & k < (i2 + 1) + 1 holds
q3 . (k + 1) = (q3 . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) ) by A3, A4, A5, A7, FINSEQ_1:def 7, NAT_1:13; :: thesis: verum

end;

hence S₁[i2 + 1] ; :: thesis: verum

end;

( len q0 = 1 & q0 . 1 = (M1 * (i,1)) * (M2 * (1,j)) ) by FINSEQ_1:39;
then A16: S₁[ 0 ] by A1;
A17: for j being Nat holds S₁[j] from NAT_1:sch 2(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 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 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