let i be Integer; :: thesis: for x being real number holds (exp_R x) #R i = exp_R (i * x)
let x be real number ; :: thesis: (exp_R x) #R i = exp_R (i * x)
consider n being Element of NAT such that
A1: ( i = n or i = - n ) by INT_1:8;

now

per cases ( i = n or i = - n ) by A1;

case i = n ; :: thesis: (exp_R x) #R i = exp_R (i * x)

hence (exp_R x) #R i = exp_R (i * x) by Lm1; :: thesis: verum

end;

case A2: i = - n ; :: thesis: exp_R (i * x) = (exp_R x) #R i

hence exp_R (i * x) = exp_R (- (n * x))
.= 1 / (exp_R (n * x)) by Th4
.= 1 / ((exp_R x) #R n) by Lm1
.= (exp_R x) #R i by A2, PREPOWER:90, SIN_COS:60 ;
:: thesis: verum

end;

end;

end;

hence (exp_R x) #R i = exp_R (i * x) ; :: thesis: verum