let f1, f2 be V183() Function of [:NAT,NAT:],ExtREAL; :: thesis: Partial_Sums (f1 + f2) = (Partial_Sums f1) + (Partial_Sums f2)
Partial_Sums (f1 + f2) = Partial_Sums_in_cod2 ((Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 f2)) by Th44;
hence Partial_Sums (f1 + f2) = (Partial_Sums f1) + (Partial_Sums f2) by Th44; :: thesis: verum