let seq be ExtREAL_sequence; :: thesis: for n being Nat holds (Partial_Sums (- seq)) . n = - ((Partial_Sums seq) . n)
let n be Nat; :: thesis: (Partial_Sums (- seq)) . n = - ((Partial_Sums seq) . n)
defpred S₁[ Nat] means (Partial_Sums (- seq)) . $1 = - ((Partial_Sums seq) . $1);
A1: dom (- seq) = NAT by FUNCT_2:def 1;
(Partial_Sums (- seq)) . 0 = (- seq) . 0 by MESFUNC9:def 1
.= - (seq . 0) by A1, MESFUNC1:def 7 ;
then A3: S₁[ 0 ] by MESFUNC9:def 1;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
(Partial_Sums (- seq)) . (k + 1) = ((Partial_Sums (- seq)) . k) + ((- seq) . (k + 1)) by MESFUNC9:def 1
.= (- ((Partial_Sums seq) . k)) + (- (seq . (k + 1))) by A1, A5, MESFUNC1:def 7
.= - (((Partial_Sums seq) . k) + (seq . (k + 1))) by XXREAL_3:9 ;
hence S₁[k + 1] by MESFUNC9:def 1; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
hence (Partial_Sums (- seq)) . n = - ((Partial_Sums seq) . n) ; :: thesis: verum