let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: for n, m being Nat holds Rseq . ((n + 1),(m + 1)) = ((((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),(m + 1))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),m))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(m + 1)))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m))
let n, m be Nat; :: thesis: Rseq . ((n + 1),(m + 1)) = ((((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),(m + 1))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),m))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(m + 1)))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m))
set CPS = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq);
set CS = Partial_Sums_in_cod2 Rseq;
A1: (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),(m + 1)) = ((Partial_Sums_in_cod2 Rseq) . ((n + 1),(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(m + 1))) by DefRS
.= ((Rseq . ((n + 1),(m + 1))) + ((Partial_Sums_in_cod2 Rseq) . ((n + 1),m))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(m + 1))) by DefCS ;
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),m) = ((Partial_Sums_in_cod2 Rseq) . ((n + 1),m)) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m)) by DefRS;
hence Rseq . ((n + 1),(m + 1)) = ((((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),(m + 1))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),m))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(m + 1)))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m)) by A1; :: thesis: verum