let x, p be real number ; :: thesis: (exp_R x) #R p = exp_R (p * x)
exp_R x > 0 by SIN_COS:60;
then consider s being Rational_Sequence such that
A1: s is convergent and
A2: lim s = p and
(exp_R x) #Q s is convergent and
A3: lim ((exp_R x) #Q s) = (exp_R x) #R p by PREPOWER:def 8;

A4: now

let ii be set ; :: thesis: ( ii in NAT implies ((exp_R x) #Q s) . ii = (exp_R /* (x (#) s)) . ii )
assume A5: ii in NAT ; :: thesis: ((exp_R x) #Q s) . ii = (exp_R /* (x (#) s)) . ii
reconsider i = ii as Element of NAT by A5;
A6: rng (x (#) s) c= dom exp_R by SIN_COS:51;
thus ((exp_R x) #Q s) . ii = (exp_R x) #Q (s . i) by PREPOWER:def 7
.= exp_R ((s . i) * x) by Th7
.= exp_R ((x (#) s) . i) by SEQ_1:13
.= exp_R . ((x (#) s) . i) by SIN_COS:def 27
.= (exp_R /* (x (#) s)) . ii by A6, FUNCT_2:185 ; :: thesis: verum

end;

A7: x (#) s is convergent by A1, SEQ_2:21;
A8: lim (x (#) s) = x * p by A1, A2, SEQ_2:22;
exp_R is_differentiable_in x * p by SIN_COS:70;
then A9: exp_R is_continuous_in x * p by FDIFF_1:32;
rng (x (#) s) c= dom exp_R by SIN_COS:51;
then lim (exp_R /* (x (#) s)) = exp_R . (x * p) by A7, A8, A9, FCONT_1:def 1
.= exp_R (p * x) by SIN_COS:def 27 ;
hence (exp_R x) #R p = exp_R (p * x) by A3, A4, FUNCT_2:18; :: thesis: verum