let i be Integer; :: thesis: for x being Real holds (exp_R x) #R i = exp_R (i * x)
let x be Real; :: thesis: (exp_R x) #R i = exp_R (i * x)
consider n being Nat such that
A1: ( i = n or i = - n ) by INT_1:2;

now :: thesis: ( ( i = n & (exp_R x) #R i = exp_R (i * x) ) or ( i = - n & exp_R (i * x) = (exp_R x) #R i ) )

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:76, SIN_COS:55 ;
:: thesis: verum

end;

end;

end;

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