for f being Function of [:NAT,NAT:],ExtREAL st ( not f is V183() or not f is V184() ) holds
Partial_Sums f = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f) by Lm8, Lm9;