theorem Th54: :: DBLSEQ_3:54

for f being Function of [:NAT,NAT:],ExtREAL st ( not f is without-infty or not f is without+infty ) holds
( ProjMap1 ((Partial_Sums f),0) = ProjMap1 ((Partial_Sums_in_cod2 f),0) & ProjMap2 ((Partial_Sums f),0) = ProjMap2 ((Partial_Sums_in_cod1 f),0) )