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 S1[ 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 S1[i2] holds
S1[i2 + 1]
proof
let i2 be 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 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 S1[i2 + 1] ; :: thesis: verum
end;
( len q0 = 1 & q0 . 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 Nat holds S1[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