let x be Real; :: 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 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