let i be Nat; :: thesis: for s being Real_Sequence st s is summable & ( for n being Nat holds 0 <= s . n ) holds
(Partial_Sums s) . i <= Sum s
let s be Real_Sequence; :: thesis: ( s is summable & ( for n being Nat holds 0 <= s . n ) implies (Partial_Sums s) . i <= Sum s )
assume A1: ( s is summable & ( for n being Nat holds 0 <= s . n ) ) ; :: thesis: (Partial_Sums s) . i <= Sum s
then A2: Sum s = ((Partial_Sums s) . i) + (Sum (s ^\ (i + 1))) by SERIES_1:15;
A3: s ^\ (i + 1) is summable by A1, SERIES_1:12;
for n being Nat holds 0 <= (s ^\ (i + 1)) . n

proof

let n be Nat; :: thesis: 0 <= (s ^\ (i + 1)) . n
0 <= s . ((i + 1) + n) by A1;
hence 0 <= (s ^\ (i + 1)) . n by NAT_1:def 3; :: thesis: verum

end;

hence (Partial_Sums s) . i <= Sum s by A2, A3, SERIES_1:18, XREAL_1:31; :: thesis: verum