theorem Th54: :: DBLSEQ_3:54

for f being Function of [:NAT,NAT:],ExtREAL st ( not f is V183() or not f is V184() ) 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) )