let f1 be without-infty Function of [:NAT,NAT:],ExtREAL; :: thesis: for f2 being without+infty Function of [:NAT,NAT:],ExtREAL holds
( 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) & Partial_Sums_in_cod2 (f2 - f1) = (Partial_Sums_in_cod2 f2) - (Partial_Sums_in_cod2 f1) & Partial_Sums_in_cod1 (f2 - f1) = (Partial_Sums_in_cod1 f2) - (Partial_Sums_in_cod1 f1) )
let f2 be without+infty 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) & Partial_Sums_in_cod2 (f2 - f1) = (Partial_Sums_in_cod2 f2) - (Partial_Sums_in_cod2 f1) & Partial_Sums_in_cod1 (f2 - f1) = (Partial_Sums_in_cod1 f2) - (Partial_Sums_in_cod1 f1) )
Partial_Sums_in_cod2 (f1 - f2) = Partial_Sums_in_cod2 (f1 + (- f2)) by Th10
.= (Partial_Sums_in_cod2 f1) + (Partial_Sums_in_cod2 (- f2)) by Th44
.= (Partial_Sums_in_cod2 f1) + (- (Partial_Sums_in_cod2 f2)) by Th42 ;
hence Partial_Sums_in_cod2 (f1 - f2) = (Partial_Sums_in_cod2 f1) - (Partial_Sums_in_cod2 f2) by Th10; :: thesis: ( Partial_Sums_in_cod1 (f1 - f2) = (Partial_Sums_in_cod1 f1) - (Partial_Sums_in_cod1 f2) & Partial_Sums_in_cod2 (f2 - f1) = (Partial_Sums_in_cod2 f2) - (Partial_Sums_in_cod2 f1) & Partial_Sums_in_cod1 (f2 - f1) = (Partial_Sums_in_cod1 f2) - (Partial_Sums_in_cod1 f1) )
Partial_Sums_in_cod1 (f1 - f2) = Partial_Sums_in_cod1 (f1 + (- f2)) by Th10
.= (Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 (- f2)) by Th44
.= (Partial_Sums_in_cod1 f1) + (- (Partial_Sums_in_cod1 f2)) by Th42 ;
hence Partial_Sums_in_cod1 (f1 - f2) = (Partial_Sums_in_cod1 f1) - (Partial_Sums_in_cod1 f2) by Th10; :: thesis: ( Partial_Sums_in_cod2 (f2 - f1) = (Partial_Sums_in_cod2 f2) - (Partial_Sums_in_cod2 f1) & Partial_Sums_in_cod1 (f2 - f1) = (Partial_Sums_in_cod1 f2) - (Partial_Sums_in_cod1 f1) )
Partial_Sums_in_cod2 (f2 - f1) = Partial_Sums_in_cod2 (f2 + (- f1)) by Th10
.= (Partial_Sums_in_cod2 f2) + (Partial_Sums_in_cod2 (- f1)) by Th45
.= (Partial_Sums_in_cod2 f2) + (- (Partial_Sums_in_cod2 f1)) by Th42 ;
hence Partial_Sums_in_cod2 (f2 - f1) = (Partial_Sums_in_cod2 f2) - (Partial_Sums_in_cod2 f1) by Th10; :: thesis: Partial_Sums_in_cod1 (f2 - f1) = (Partial_Sums_in_cod1 f2) - (Partial_Sums_in_cod1 f1)
Partial_Sums_in_cod1 (f2 - f1) = Partial_Sums_in_cod1 (f2 + (- f1)) by Th10
.= (Partial_Sums_in_cod1 f2) + (Partial_Sums_in_cod1 (- f1)) by Th45
.= (Partial_Sums_in_cod1 f2) + (- (Partial_Sums_in_cod1 f1)) by Th42 ;
hence Partial_Sums_in_cod1 (f2 - f1) = (Partial_Sums_in_cod1 f2) - (Partial_Sums_in_cod1 f1) by Th10; :: thesis: verum