theorem th100: :: DBLSEQ_2:18

for Rseq being Function of [:NAT,NAT:],REAL
for m, n being Element of NAT holds
( (Partial_Sums_in_cod1 Rseq) . (m,n) = (Partial_Sums (ProjMap2 (Rseq,n))) . m & (Partial_Sums_in_cod2 Rseq) . (m,n) = (Partial_Sums (ProjMap1 (Rseq,m))) . n )