let n be Element of NAT ; :: thesis: (n ! ) * (Sum (eseq ^\ (n + 1))) > 0
A1: n ! > 0 by NEWTON:23;
A2: eseq ^\ (n + 1) is summable by Th24, SERIES_1:15;

now

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

end;

then Sum (eseq ^\ (n + 1)) > 0 by A2, Th35;
hence (n ! ) * (Sum (eseq ^\ (n + 1))) > 0 by A1, XREAL_1:131; :: thesis: verum