theorem :: DBLSEQ_2:14

for Rseq being Function of [:NAT,NAT:],REAL
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))