let K be Element of NAT ; :: thesis: for seq being Real_Sequence st seq is summable & ( for k being Element of NAT holds seq . k >= 0 ) holds
Sum seq >= (Partial_Sums seq) . K
let seq be Real_Sequence; :: thesis: ( seq is summable & ( for k being Element of NAT holds seq . k >= 0 ) implies Sum seq >= (Partial_Sums seq) . K )
assume A1: ( seq is summable & ( for k being Element of NAT holds seq . k >= 0 ) ) ; :: thesis: Sum seq >= (Partial_Sums seq) . K
then A2: seq ^\ (K + 1) is summable by SERIES_1:15;

now

let k be Element of NAT ; :: thesis: (seq ^\ (K + 1)) . k >= 0
(seq ^\ (K + 1)) . k = seq . ((K + 1) + k) by NAT_1:def 3;
hence (seq ^\ (K + 1)) . k >= 0 by A1; :: thesis: verum

end;

then Sum (seq ^\ (K + 1)) >= 0 by A2, SERIES_1:21;
then ((Partial_Sums seq) . K) + (Sum (seq ^\ (K + 1))) >= ((Partial_Sums seq) . K) + 0 by XREAL_1:8;
hence Sum seq >= (Partial_Sums seq) . K by A1, SERIES_1:18; :: thesis: verum