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