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