theorem th00: :: DBLSEQ_2:19

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