let seq be Real_Sequence; :: thesis: ( seq is summable & ( for n being Nat holds seq . n > 0 ) implies Sum seq > 0 )
assume that
A1: seq is summable and
A2: for n being Nat holds seq . n > 0 ; :: thesis: Sum seq > 0
A3: Sum seq = ((Partial_Sums seq) . 0) + (Sum (seq ^\ (0 + 1))) by A1, SERIES_1:15
.= (seq . 0) + (Sum (seq ^\ 1)) by SERIES_1:def 1 ;
A4: now :: thesis: for n being Nat holds (seq ^\ 1) . n >= 0
let n be Nat; :: thesis: (seq ^\ 1) . n >= 0
(seq ^\ 1) . n = seq . (1 + n) by NAT_1:def 3;
hence (seq ^\ 1) . n >= 0 by A2; :: thesis: verum
end;
seq ^\ 1 is summable by A1, SERIES_1:12;
then Sum (seq ^\ 1) >= 0 by A4, SERIES_1:18;
then Sum seq > 0 + 0 by A2, A3, XREAL_1:8;
hence Sum seq > 0 ; :: thesis: verum