let n be Element of NAT ; :: thesis: (n ! ) * (Sum (eseq ^\ (n + 1))) > 0

A1: now

let k be Element of NAT ; :: thesis: (eseq ^\ (n + 1)) . k > 0
A2: ((n + 1) + k) ! > 0 by NEWTON:23;
(eseq ^\ (n + 1)) . k = eseq . ((n + 1) + k) by NAT_1:def 3
.= 1 / (((n + 1) + k) ! ) by Def5 ;
hence (eseq ^\ (n + 1)) . k > 0 by A2; :: thesis: verum

end;

eseq ^\ (n + 1) is summable by Th24, SERIES_1:15;
then ( n ! > 0 & Sum (eseq ^\ (n + 1)) > 0 ) by A1, Th35, NEWTON:23;
hence (n ! ) * (Sum (eseq ^\ (n + 1))) > 0 by XREAL_1:131; :: thesis: verum