let n be Nat; :: thesis: (n !) * (Sum (eseq ^\ (n + 1))) > 0
A1: now :: thesis: for k being Nat holds (eseq ^\ (n + 1)) . k > 0
let k be 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 Th23, SERIES_1:12;
then ( n ! > 0 & Sum (eseq ^\ (n + 1)) > 0 ) by A1, Th34;
hence (n !) * (Sum (eseq ^\ (n + 1))) > 0 by XREAL_1:129; :: thesis: verum