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 S₁[ 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 S₁[i2] holds
S₁[i2 + 1]

proof

let i2 be Element of 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 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)) ) )

per cases 1 <= i2 + 1 by NAT_1:12;

suppose A5: 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:35
.= (i2 + 1) + 1 by A3, A4, A5, FINSEQ_1:56, 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;

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

suppose A11: 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:35;
then k2 < (len q2) + 1 by FINSEQ_1:56;
then k2 <= len q2 by NAT_1:13;
then k2 in dom q2 by A8, FINSEQ_3:27;
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:8;
then k2 + 1 < (len q2) + (len <*((q2 . (i2 + 1)) + ((M1 * i,((i2 + 1) + 1)) * (M2 * ((i2 + 1) + 1),j)))*>) by A6, FINSEQ_1:35;
then k2 + 1 < (len q2) + 1 by FINSEQ_1:56;
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:27;
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;

suppose A14: 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:35;
then k2 < (len q2) + 1 by FINSEQ_1:56;
then k2 <= len q2 by NAT_1:13;
then k2 in dom q2 by A8, FINSEQ_3:27;
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:5;
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:55, 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:35;
then 1 < (len q2) + 1 by FINSEQ_1:56;
then 1 <= len q2 by NAT_1:13;
then 1 in dom q2 by FINSEQ_3:27;
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 S₁[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:56, FINSEQ_1:def 8;
then A16: S₁[ 0 ] by A1;
A17: for j being Element of NAT holds S₁[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:11;
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