let p, x be Real; :: thesis: (exp_R x) #R p = exp_R (p * x)
exp_R x > 0 by SIN_COS:55;
then consider s being Rational_Sequence such that
A1: ( s is convergent & lim s = p ) and
(exp_R x) #Q s is convergent and
A2: lim ((exp_R x) #Q s) = (exp_R x) #R p by PREPOWER:def 7;
A3: ( exp_R is_continuous_in x * p & rng (x (#) s) c= dom exp_R ) by FDIFF_1:24, SIN_COS:47, SIN_COS:65;
A4: now :: thesis: for ii being object st ii in NAT holds
((exp_R x) #Q s) . ii = (exp_R /* (x (#) s)) . ii
let ii be object ; :: thesis: ( ii in NAT implies ((exp_R x) #Q s) . ii = (exp_R /* (x (#) s)) . ii )
assume ii in NAT ; :: thesis: ((exp_R x) #Q s) . ii = (exp_R /* (x (#) s)) . ii
then reconsider i = ii as Element of NAT ;
A5: rng (x (#) s) c= dom exp_R by SIN_COS:47;
thus ((exp_R x) #Q s) . ii = (exp_R x) #Q (s . i) by PREPOWER:def 6
.= exp_R ((s . i) * x) by Th7
.= exp_R ((x (#) s) . i) by SEQ_1:9
.= exp_R . ((x (#) s) . i) by SIN_COS:def 23
.= (exp_R /* (x (#) s)) . ii by A5, FUNCT_2:108 ; :: thesis: verum
end;
( x (#) s is convergent & lim (x (#) s) = x * p ) by A1, SEQ_2:7, SEQ_2:8;
then lim (exp_R /* (x (#) s)) = exp_R . (x * p) by A3, FCONT_1:def 1
.= exp_R (p * x) by SIN_COS:def 23 ;
hence (exp_R x) #R p = exp_R (p * x) by A2, A4, FUNCT_2:12; :: thesis: verum