let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: for m, n being Nat holds (Partial_Sums Rseq) . (m,n) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (m,n)
defpred S1[ Nat] means for m being Nat holds (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (m,$1) = (Partial_Sums Rseq) . (m,$1);
defpred S2[ Nat] means (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ($1,0) = (Partial_Sums Rseq) . ($1,0);
Y3: (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,0) = (Partial_Sums_in_cod2 Rseq) . (0,0) by DefRS
.= Rseq . (0,0) by DefCS ;
(Partial_Sums Rseq) . (0,0) = (Partial_Sums_in_cod1 Rseq) . (0,0) by DefCS
.= Rseq . (0,0) by DefRS ;
then Y1: S2[ 0 ] by Y3;
Y2: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume Y3: S2[i] ; :: thesis: S2[i + 1]
Y4: (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((i + 1),0) = ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (i,0)) + ((Partial_Sums_in_cod2 Rseq) . ((i + 1),0)) by DefRS
.= ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (i,0)) + (Rseq . ((i + 1),0)) by DefCS ;
(Partial_Sums Rseq) . ((i + 1),0) = (Partial_Sums_in_cod1 Rseq) . ((i + 1),0) by DefCS
.= ((Partial_Sums_in_cod1 Rseq) . (i,0)) + (Rseq . ((i + 1),0)) by DefRS
.= ((Partial_Sums Rseq) . (i,0)) + (Rseq . ((i + 1),0)) by DefCS ;
hence S2[i + 1] by Y3, Y4; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(Y1, Y2);
 then X1: S1[ 0 ] ;
X2: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume Z3: S1[j] ; :: thesis: S1[j + 1]
for m being Nat holds (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (m,(j + 1)) = (Partial_Sums Rseq) . (m,(j + 1))
proof
let n be Nat; :: thesis: (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(j + 1)) = (Partial_Sums Rseq) . (n,(j + 1))
defpred S3[ Nat] means (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ($1,(j + 1)) = (Partial_Sums Rseq) . ($1,(j + 1));
Z4: (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,(j + 1)) = (Partial_Sums_in_cod2 Rseq) . (0,(j + 1)) by DefRS
.= ((Partial_Sums_in_cod2 Rseq) . (0,j)) + (Rseq . (0,(j + 1))) by DefCS
.= ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,j)) + (Rseq . (0,(j + 1))) by DefRS ;
(Partial_Sums Rseq) . (0,(j + 1)) = ((Partial_Sums Rseq) . (0,j)) + ((Partial_Sums_in_cod1 Rseq) . (0,(j + 1))) by DefCS
.= ((Partial_Sums Rseq) . (0,j)) + (Rseq . (0,(j + 1))) by DefRS
.= ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,j)) + (Rseq . (0,(j + 1))) by Z3 ;
then Z1: S3[ 0 ] by Z4;
Z2: for i being Nat st S3[i] holds
S3[i + 1]
proof
let i be Nat; :: thesis: ( S3[i] implies S3[i + 1] )
assume S3[i] ; :: thesis: S3[i + 1]
Z6: (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (i,j) = (Partial_Sums Rseq) . (i,j) by Z3;
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((i + 1),(j + 1)) = ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (i,(j + 1))) + ((Partial_Sums_in_cod2 Rseq) . ((i + 1),(j + 1))) by DefRS
.= (((Partial_Sums Rseq) . (i,j)) + ((Partial_Sums_in_cod1 Rseq) . (i,(j + 1)))) + ((Partial_Sums_in_cod2 Rseq) . ((i + 1),(j + 1))) by Z6, ThRS
.= (((Partial_Sums Rseq) . (i,j)) + ((Partial_Sums_in_cod1 Rseq) . (i,(j + 1)))) + (((Partial_Sums_in_cod2 Rseq) . ((i + 1),j)) + (Rseq . ((i + 1),(j + 1)))) by DefCS
.= (((Partial_Sums Rseq) . (i,j)) + (((Partial_Sums_in_cod1 Rseq) . (i,(j + 1))) + (Rseq . ((i + 1),(j + 1))))) + ((Partial_Sums_in_cod2 Rseq) . ((i + 1),j))
.= (((Partial_Sums Rseq) . (i,j)) + ((Partial_Sums_in_cod1 Rseq) . ((i + 1),(j + 1)))) + ((Partial_Sums_in_cod2 Rseq) . ((i + 1),j)) by DefRS
.= (((Partial_Sums Rseq) . (i,j)) + ((Partial_Sums_in_cod2 Rseq) . ((i + 1),j))) + ((Partial_Sums_in_cod1 Rseq) . ((i + 1),(j + 1)))
.= ((Partial_Sums Rseq) . ((i + 1),j)) + ((Partial_Sums_in_cod1 Rseq) . ((i + 1),(j + 1))) by ThRS ;
hence S3[i + 1] by DefCS; :: thesis: verum
end;
for n being Nat holds S3[n] from NAT_1:sch 2(Z1, Z2);
 hence (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(j + 1)) = (Partial_Sums Rseq) . (n,(j + 1)) ; :: thesis: verum
end;
hence S1[j + 1] ; :: thesis: verum
end;
for m being Nat holds S1[m] from NAT_1:sch 2(X1, X2);
 hence for m, n being Nat holds (Partial_Sums Rseq) . (m,n) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (m,n) ; :: thesis: verum