for f being Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums_in_cod2 (- f) = - (Partial_Sums_in_cod2 f) & Partial_Sums_in_cod1 (- f) = - (Partial_Sums_in_cod1 f) )