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

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