let f be without+infty Function of [:NAT,NAT:],ExtREAL; :: thesis: Partial_Sums f = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)
reconsider g = - f as without-infty Function of [:NAT,NAT:],ExtREAL ;
A1: Partial_Sums f = Partial_Sums (- g) by Th2
.= Partial_Sums_in_cod2 (- (Partial_Sums_in_cod1 g)) by Th42
.= - (Partial_Sums g) by Th42 ;
Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f) = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 (- g)) by Th2
.= Partial_Sums_in_cod1 (- (Partial_Sums_in_cod2 g)) by Th42
.= - (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 g)) by Th42 ;
hence Partial_Sums f = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f) by A1, Lm8; :: thesis: verum