let seq be ExtREAL_sequence; :: thesis: Partial_Sums (- seq) = - (Partial_Sums seq)

now :: thesis: for n being Element of NAT holds (Partial_Sums (- seq)) . n = (- (Partial_Sums seq)) . n

hence
Partial_Sums (- seq) = - (Partial_Sums seq)
by FUNCT_2:def 8; :: thesis: verumlet n be Element of NAT ; :: thesis: (Partial_Sums (- seq)) . n = (- (Partial_Sums seq)) . n

A1: dom (- (Partial_Sums seq)) = NAT by FUNCT_2:def 1;

(Partial_Sums (- seq)) . n = - ((Partial_Sums seq) . n) by Th43;

hence (Partial_Sums (- seq)) . n = (- (Partial_Sums seq)) . n by A1, MESFUNC1:def 7; :: thesis: verum

end;A1: dom (- (Partial_Sums seq)) = NAT by FUNCT_2:def 1;

(Partial_Sums (- seq)) . n = - ((Partial_Sums seq) . n) by Th43;

hence (Partial_Sums (- seq)) . n = (- (Partial_Sums seq)) . n by A1, MESFUNC1:def 7; :: thesis: verum