let M, L be Real; :: thesis: ( M >= 0 & L >= 0 implies for e being Real st e > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(M * (L |^ m)) / (m ! ) < e )
assume A1: ( M >= 0 & L >= 0 ) ; :: thesis: for e being Real st e > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(M * (L |^ m)) / (m ! ) < e
A2: 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 9
.= (M (#) (L rExpSeq )) . n by SEQ_1:13 ;
hence M * ((L |^ n) / (n ! )) = (M (#) (L rExpSeq )) . n ; :: thesis: verum

end;

L rExpSeq is summable by SIN_COS:49;
then ( L rExpSeq is convergent & lim (L rExpSeq ) = 0 ) by SERIES_1:7;
then A3: ( M (#) (L rExpSeq ) is convergent & lim (M (#) (L rExpSeq )) = M * 0 ) by SEQ_2:21, SEQ_2:22;
let p be Real; :: thesis: ( p > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(M * (L |^ m)) / (m ! ) < p )
assume A4: p > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(M * (L |^ m)) / (m ! ) < p
consider n being Element of NAT such that
A5: for m being Element of NAT st n <= m holds
abs (((M (#) (L rExpSeq )) . m) - 0 ) < p by A3, A4, SEQ_2:def 7;
take n ; :: thesis: for m being Element of NAT st n <= m holds
(M * (L |^ m)) / (m ! ) < p

now

let m be Element of NAT ; :: thesis: ( n <= m implies (M * (L |^ m)) / (m ! ) < p )
assume A6: n <= m ; :: thesis: (M * (L |^ m)) / (m ! ) < p
A7: L |^ m >= 0 by A1, POWER:3;
m ! > 0 by NEWTON:23;
then A8: (L |^ m) / (m ! ) >= 0 by A7;
abs (((M (#) (L rExpSeq )) . m) - 0 ) = abs (M * ((L |^ m) / (m ! ))) by A2
.= (abs M) * (abs ((L |^ m) / (m ! ))) by COMPLEX1:151
.= M * (abs ((L |^ m) / (m ! ))) by A1, ABSVALUE:def 1
.= M * ((L |^ m) / (m ! )) by A8, ABSVALUE:def 1
.= (M * (L |^ m)) / (m ! ) by XCMPLX_1:75 ;
hence (M * (L |^ m)) / (m ! ) < p by A5, A6; :: thesis: verum

end;

hence for m being Element of NAT st n <= m holds
(M * (L |^ m)) / (m ! ) < p ; :: thesis: verum