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

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