let f1, f2 be V184() Function of [:NAT,NAT:],ExtREAL; :: thesis: ( Partial_Sums_in_cod2 (f1 + f2) = (Partial_Sums_in_cod2 f1) + (Partial_Sums_in_cod2 f2) & Partial_Sums_in_cod1 (f1 + f2) = (Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 f2) )
reconsider F1 = - f1, F2 = - f2 as V183() Function of [:NAT,NAT:],ExtREAL ;
F1 + F2 = (- f1) - f2 by Th10
.= - (f1 + f2) by Th9 ;
then A1: - (F1 + F2) = f1 + f2 by Th2;
then Partial_Sums_in_cod2 (f1 + f2) = - (Partial_Sums_in_cod2 (F1 + F2)) by Th42
.= - ((Partial_Sums_in_cod2 F1) + (Partial_Sums_in_cod2 F2)) by Th44
.= - ((- (Partial_Sums_in_cod2 f1)) + (Partial_Sums_in_cod2 F2)) by Th42
.= - ((- (Partial_Sums_in_cod2 f1)) + (- (Partial_Sums_in_cod2 f2))) by Th42
.= (- (- (Partial_Sums_in_cod2 f1))) - (- (Partial_Sums_in_cod2 f2)) by Th8
.= (Partial_Sums_in_cod2 f1) - (- (Partial_Sums_in_cod2 f2)) by Th2
.= (Partial_Sums_in_cod2 f1) + (- (- (Partial_Sums_in_cod2 f2))) by Th10 ;
hence Partial_Sums_in_cod2 (f1 + f2) = (Partial_Sums_in_cod2 f1) + (Partial_Sums_in_cod2 f2) by Th2; :: thesis: Partial_Sums_in_cod1 (f1 + f2) = (Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 f2)
Partial_Sums_in_cod1 (f1 + f2) = - (Partial_Sums_in_cod1 (F1 + F2)) by A1, Th42
.= - ((Partial_Sums_in_cod1 F1) + (Partial_Sums_in_cod1 F2)) by Th44
.= - ((- (Partial_Sums_in_cod1 f1)) + (Partial_Sums_in_cod1 F2)) by Th42
.= - ((- (Partial_Sums_in_cod1 f1)) + (- (Partial_Sums_in_cod1 f2))) by Th42
.= (- (- (Partial_Sums_in_cod1 f1))) - (- (Partial_Sums_in_cod1 f2)) by Th8
.= (Partial_Sums_in_cod1 f1) - (- (Partial_Sums_in_cod1 f2)) by Th2
.= (Partial_Sums_in_cod1 f1) + (- (- (Partial_Sums_in_cod1 f2))) by Th10 ;
hence Partial_Sums_in_cod1 (f1 + f2) = (Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 f2) by Th2; :: thesis: verum