let n be Nat; :: thesis: for x being Real holds (exp_R x) #R n = exp_R (n * x)
let x be Real; :: thesis: (exp_R x) #R n = exp_R (n * x)
reconsider x = x as Real ;
defpred S₁[ Nat] means (exp_R x) #R $1 = exp_R ($1 * x);
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
thus (exp_R x) #R (k + 1) = ((exp_R x) #R k) * ((exp_R x) #R 1) by PREPOWER:75, SIN_COS:55
.= ((exp_R x) #R k) * (exp_R x) by PREPOWER:72, SIN_COS:55
.= exp_R ((k1 * x) + x) by A2, SIN_COS:50
.= exp_R ((k + 1) * x) ; :: thesis: verum

end;

A3: S₁[ 0 ] by PREPOWER:71, SIN_COS:51, SIN_COS:55;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence (exp_R x) #R n = exp_R (n * x) ; :: thesis: verum