let x be real number ; :: thesis: for q being Rational holds (exp_R x) #R q = exp_R (q * x)
let q be Rational; :: thesis: (exp_R x) #R q = exp_R (q * x)
consider m being Integer, n being Element of NAT such that
n <> 0 and
A1: q = m / n by RAT_1:24;
thus (exp_R x) #R q = exp_R (q * x) by A1, Th6; :: thesis: verum