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 S1[ 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 ;
then A3: S1[ 0 ] by MESFUNC9:def 1;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[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
.= - (((Partial_Sums seq) . k) + (seq . (k + 1))) by XXREAL_3:9 ;
hence S1[k + 1] by MESFUNC9:def 1; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A3, A4);
hence (Partial_Sums (- seq)) . n = - ((Partial_Sums seq) . n) ; :: thesis: verum