theorem Th45: :: E_TRANS2:39

for m being positive Nat
for M being non zero Nat
for z0 being non zero Element of F_Real st z0 = number_e holds
ex n1 being Nat st
for n being Nat st n1 <= n holds
|.((((m |^ (m + 1)) |^ n) / (n !)) - 0).| < 1 / (2 * (M * (z0 to_power m)))