let i be Integer; :: thesis: for x being real number holds (exp_R x) #R (1 / i) = exp_R (x / i)
let x be real number ; :: thesis: (exp_R x) #R (1 / i) = exp_R (x / i)
set n = i;

per cases ( i <> 0 or i = 0 ) ;

suppose A1: i <> 0 ; :: thesis: (exp_R x) #R (1 / i) = exp_R (x / i)

then exp_R x = exp_R ((x / i) * i) by XCMPLX_1:88
.= (exp_R (x / i)) #R i by Lm2 ;
hence (exp_R x) #R (1 / i) = (exp_R (x / i)) #R (i * (1 / i)) by PREPOWER:105, SIN_COS:60
.= (exp_R (x / i)) #R 1 by A1, XCMPLX_1:107
.= exp_R (x / i) by PREPOWER:86, SIN_COS:60 ;
:: thesis: verum

end;

suppose A2: i = 0 ; :: thesis: (exp_R x) #R (1 / i) = exp_R (x / i)

(exp_R x) #R (1 / 0 ) = exp_R 0 by PREPOWER:85, SIN_COS:56, SIN_COS:60
.= exp_R (x / 0 ) by XCMPLX_1:49 ;
hence (exp_R x) #R (1 / i) = exp_R (x / i) by A2; :: thesis: verum

end;

end;