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 (#) (L rExpSeq) is convergent by SEQ_2:7, SERIES_1:4;
lim (L rExpSeq) = 0 by A3, SERIES_1:4;
then A5: lim (M (#) (L rExpSeq)) = M * 0 by A3, SEQ_2:8, SERIES_1:4;
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 (#) (L rExpSeq)) . m) - 0).| < p by A4, A5, SEQ_2:def 7;
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 (#) (L rExpSeq)) . n

proof

let n be Element of NAT ; :: thesis: M * ((L |^ n) / (n !)) = (M (#) (L rExpSeq)) . n
M * ((L |^ n) / (n !)) = M * ((L rExpSeq) . n) by SIN_COS:def 5
.= (M (#) (L rExpSeq)) . n by SEQ_1:9 ;
hence M * ((L |^ n) / (n !)) = (M (#) (L rExpSeq)) . 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 A2, POWER:3;
|.(((M (#) (L rExpSeq)) . m) - 0).| = |.(M * ((L |^ m) / (m !))).| by A7, A9
.= |.M.| * |.((L |^ m) / (m !)).| by COMPLEX1:65
.= M * |.((L |^ m) / (m !)).| by A1, ABSVALUE:def 1
.= M * ((L |^ m) / (m !)) by A10, ABSVALUE:def 1
.= (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