let seq be nonnegative 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
defpred S₁[ Nat] means seq . $1 <= (Partial_Sums seq) . $1;
A1: S₁[ 0 ] by MESFUNC9:def 1;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
(Partial_Sums seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by MESFUNC9:def 1;
hence S₁[k + 1] by XXREAL_3:39, SUPINF_2:51; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence seq . m <= (Partial_Sums seq) . m ; :: thesis: verum