let x be Real; :: thesis: for q being Rational holds (exp_R x) #Q q = exp_R (q * x)
let q be Rational; :: thesis: (exp_R x) #Q q = exp_R (q * x)
thus (exp_R x) #Q q = (exp_R x) #R q by PREPOWER:74, SIN_COS:55
.= exp_R (q * x) by Lm3 ; :: thesis: verum