theorem Th35: :: IRRAT_1:35
for n being Nat holds (n !) * (Sum (eseq ^\ (n + 1))) > 0