theorem Th12: :: TAYLOR_2:12

for M, L being Real st M >= 0 & L >= 0 holds
for e being Real st e > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
(M * (L |^ m)) / (m !) < e