let x be Real; :: thesis: ( (exp_R 1) #R x = exp_R x & (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x )
thus A1: exp_R x = exp_R (x * 1)
.= (exp_R 1) #R x by Th8 ; :: thesis: ( (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x )
exp_R 1 > 0 by SIN_COS:55;
hence ( (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x ) by A1, IRRAT_1:def 7, POWER:def 2; :: thesis: verum