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
let 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;
hence Partial_Sums (- seq) = - (Partial_Sums seq) by FUNCT_2:def 8; :: thesis: verum