let f1 be without-infty Function of [:NAT,NAT:],ExtREAL; :: thesis: for f2 being without+infty Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums (f1 - f2) = (Partial_Sums f1) - (Partial_Sums f2) & Partial_Sums (f2 - f1) = (Partial_Sums f2) - (Partial_Sums f1) )
let f2 be without+infty Function of [:NAT,NAT:],ExtREAL; :: thesis: ( Partial_Sums (f1 - f2) = (Partial_Sums f1) - (Partial_Sums f2) & Partial_Sums (f2 - f1) = (Partial_Sums f2) - (Partial_Sums f1) )
Partial_Sums (f1 - f2) = Partial_Sums_in_cod2 ((Partial_Sums_in_cod1 f1) - (Partial_Sums_in_cod1 f2)) by Th46;
hence Partial_Sums (f1 - f2) = (Partial_Sums f1) - (Partial_Sums f2) by Th46; :: thesis: Partial_Sums (f2 - f1) = (Partial_Sums f2) - (Partial_Sums f1)
Partial_Sums (f2 - f1) = Partial_Sums_in_cod2 ((Partial_Sums_in_cod1 f2) - (Partial_Sums_in_cod1 f1)) by Th46;
hence Partial_Sums (f2 - f1) = (Partial_Sums f2) - (Partial_Sums f1) by Th46; :: thesis: verum