theorem thRS2: :: DBLSEQ_2:13

for Rseq being 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))