let x, a 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:55, TAYLOR_1:11
.= exp_R . (log (number_e,(a #R x))) by A1, POWER:def 2
.= a #R x by A1, PREPOWER:81, TAYLOR_1:15 ;
hence exp_R . (x * (log (number_e,a))) = a #R x ; :: thesis: verum