:: deftheorem defines Partial_Sums DBLSEQ_2:def 4 :
for Rseq being Function of [:NAT,NAT:],REAL holds Partial_Sums Rseq = Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq);