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

now

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

end;

then Sum (seq ^\ 1) >= 0 by A3, SERIES_1:21;
then Sum seq > 0 + 0 by A1, A2, XREAL_1:10;
hence Sum seq > 0 ; :: thesis: verum