theorem ThRS: :: DBLSEQ_2:11

for Rseq being Function of [:NAT,NAT:],REAL
for n, m being Nat holds
( (Partial_Sums Rseq) . ((n + 1),m) = ((Partial_Sums_in_cod2 Rseq) . ((n + 1),m)) + ((Partial_Sums Rseq) . (n,m)) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 Rseq) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m)) )