let M, L be Real; :: thesis: ( M >= 0 & L >= 0 implies 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 )

assume that
A1: M >= 0 and
A2: L >= 0 ; :: thesis: 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

A3: L rExpSeq is summable by SIN_COS:45;
then A4: M (#) () is convergent by ;
lim () = 0 by ;
then A5: lim (M (#) ()) = M * 0 by ;
let p be Real; :: thesis: ( p > 0 implies ex n being Nat st
for m being Nat st n <= m holds
(M * (L |^ m)) / (m !) < p )

assume p > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
(M * (L |^ m)) / (m !) < p

then consider n being Nat such that
A6: for m being Nat st n <= m holds
|.(((M (#) ()) . m) - 0).| < p by ;
take n ; :: thesis: for m being Nat st n <= m holds
(M * (L |^ m)) / (m !) < p

A7: for n being Element of NAT holds M * ((L |^ n) / (n !)) = (M (#) ()) . n
proof
let n be Element of NAT ; :: thesis: M * ((L |^ n) / (n !)) = (M (#) ()) . n
M * ((L |^ n) / (n !)) = M * (() . n) by SIN_COS:def 5
.= (M (#) ()) . n by SEQ_1:9 ;
hence M * ((L |^ n) / (n !)) = (M (#) ()) . n ; :: thesis: verum
end;
now :: thesis: for m being Nat st n <= m holds
(M * (L |^ m)) / (m !) < p
let m be Nat; :: thesis: ( n <= m implies (M * (L |^ m)) / (m !) < p )
assume A8: n <= m ; :: thesis: (M * (L |^ m)) / (m !) < p
A9: m in NAT by ORDINAL1:def 12;
A10: ( L |^ m >= 0 & m ! > 0 ) by ;
|.(((M (#) ()) . m) - 0).| = |.(M * ((L |^ m) / (m !))).| by A7, A9
.= |.M.| * |.((L |^ m) / (m !)).| by COMPLEX1:65
.= M * |.((L |^ m) / (m !)).| by
.= M * ((L |^ m) / (m !)) by
.= (M * (L |^ m)) / (m !) by XCMPLX_1:74 ;
hence (M * (L |^ m)) / (m !) < p by A6, A8; :: thesis: verum
end;
hence for m being Nat st n <= m holds
(M * (L |^ m)) / (m !) < p ; :: thesis: verum