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)
ex m being Integer ex n being Element of NAT st
( n <> 0 & q = m / n ) by RAT_1:8;
hence (exp_R x) #R q = exp_R (q * x) by Th6; :: thesis: verum