:: deftheorem defines Partial_Sums DBLSEQ_3:def 16 :
for f being Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f = Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f);