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