let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: 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; :: thesis: 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; :: thesis: verum