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