let x be Real; :: thesis: for m, n being Integer holds (exp_R x) #R (m / n) = exp_R ((m / n) * x)
let m, n be Integer; :: thesis: (exp_R x) #R (m / n) = exp_R ((m / n) * x)
thus exp_R ((m / n) * x) = exp_R ((x / n) * m) by XCMPLX_1:75
.= (exp_R (x / n)) #R m by Lm2
.= ((exp_R x) #R (1 / n)) #R m by Th5
.= (exp_R x) #R ((1 / n) * m) by PREPOWER:91, SIN_COS:55
.= (exp_R x) #R ((m / n) * 1) by XCMPLX_1:75
.= (exp_R x) #R (m / n) ; :: thesis: verum