theorem :: DBLSEQ_3:53

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