let seq be nonpositive ExtREAL_sequence; :: thesis: for m being Nat holds seq . m >= (Partial_Sums seq) . m
let m be Nat; :: thesis: seq . m >= (Partial_Sums seq) . m
reconsider f = - seq as nonnegative ExtREAL_sequence ;
A1: ( dom f = NAT & dom seq = NAT & dom (- f) = NAT & dom (Partial_Sums seq) = NAT & dom (- (Partial_Sums seq)) = NAT & dom (- (- (Partial_Sums seq))) = NAT ) by FUNCT_2:def 1;
A2: m in NAT by ORDINAL1:def 12;
f . m <= (Partial_Sums f) . m by Th4;
then f . m <= (- (Partial_Sums seq)) . m by Th1;
then - ((- seq) . m) >= - ((- (Partial_Sums seq)) . m) by XXREAL_3:38;
then (- (- seq)) . m >= - ((- (Partial_Sums seq)) . m) by A1, A2, MESFUNC1:def 7;
then seq . m >= - ((- (Partial_Sums seq)) . m) by Th2;
then seq . m >= - (- ((Partial_Sums seq) . m)) by A1, A2, MESFUNC1:def 7;
hence seq . m >= (Partial_Sums seq) . m ; :: thesis: verum