for f1, f2 being V183() Function of [:NAT,NAT:],ExtREAL holds Partial_Sums (f1 + f2) = (Partial_Sums f1) + (Partial_Sums f2)