let a, x be Real; :: thesis: ( a > 0 implies exp_R . (x * (log number_e ,a)) = a #R x )
assume A1: a > 0 ; :: thesis: exp_R . (x * (log number_e ,a)) = a #R x
number_e <> 1 by TAYLOR_1:11;
then exp_R . (x * (log number_e ,a)) = exp_R . (log number_e ,(a to_power x)) by A1, POWER:63, TAYLOR_1:11
.= exp_R . (log number_e ,(a #R x)) by A1, POWER:def 2
.= a #R x by A1, PREPOWER:95, TAYLOR_1:15 ;
hence exp_R . (x * (log number_e ,a)) = a #R x ; :: thesis: verum