let rseq be Real_Sequence; :: thesis: for m being Nat st rseq is nonnegative holds
rseq . m <= (Partial_Sums rseq) . m
let m be Nat; :: thesis: ( rseq is nonnegative implies rseq . m <= (Partial_Sums rseq) . m )
assume A1: rseq is nonnegative ; :: thesis: rseq . m <= (Partial_Sums rseq) . m
defpred S₁[ Nat] means rseq . $1 <= (Partial_Sums rseq) . $1;
a3: S₁[ 0 ] by SERIES_1: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 S₁[k] ; :: thesis: S₁[k + 1]
(Partial_Sums rseq) . (k + 1) = ((Partial_Sums rseq) . k) + (rseq . (k + 1)) by SERIES_1:def 1;
hence S₁[k + 1] by XREAL_1:31, SERIES_3:34, A1; :: thesis: verum

end;

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