theorem th103a: :: DBLSEQ_2:12

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