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
(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 ; :: thesis: verum

end;

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