let seq be ExtREAL_sequence; :: thesis: Partial_Sums (- seq) = - (Partial_Sums seq)
A1: ( dom (- seq) = NAT & dom (- (Partial_Sums seq)) = NAT ) by FUNCT_2:def 1;
defpred S1[ Nat] means (- (Partial_Sums seq)) . $1 = - ((Partial_Sums seq) . $1);
A3: S1[ 0 ] by A1, MESFUNC1:def 7;
A4: for n being Nat st S1[n] holds
S1[n + 1] by A1, MESFUNC1:def 7;
A5: for n being Nat holds S1[n] from NAT_1:sch 2(A3, A4);
 defpred S2[ Nat] means (Partial_Sums (- seq)) . $1 = (- (Partial_Sums seq)) . $1;
(Partial_Sums (- seq)) . 0 = (- seq) . 0 by MESFUNC9:def 1;
then A6: (Partial_Sums (- seq)) . 0 = - (seq . 0) by A1, MESFUNC1:def 7;
(Partial_Sums seq) . 0 = seq . 0 by MESFUNC9:def 1;
then A7: S2[ 0 ] by A1, A6, MESFUNC1:def 7;
A8: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A9: S2[n] ; :: thesis: S2[n + 1]
(Partial_Sums (- seq)) . (n + 1) = ((- (Partial_Sums seq)) . n) + ((- seq) . (n + 1)) by A9, MESFUNC9:def 1
.= ((- (Partial_Sums seq)) . n) + (- (seq . (n + 1))) by A1, MESFUNC1:def 7
.= (- ((Partial_Sums seq) . n)) - (seq . (n + 1)) by A5
.= - (((Partial_Sums seq) . n) + (seq . (n + 1))) by XXREAL_3:25
.= - ((Partial_Sums seq) . (n + 1)) by MESFUNC9:def 1 ;
hence S2[n + 1] by A1, MESFUNC1:def 7; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A7, A8);
 then 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: verum