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_{1}[ Nat] means (exp_R x) #R $1 = exp_R ($1 * x);

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by PREPOWER:71, SIN_COS:51, SIN_COS:55;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A3, A1);

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

let x be Real; :: thesis: (exp_R x) #R n = exp_R (n * x)

reconsider x = x as Real ;

defpred S

A1: for k being Nat st S

S

proof

A3:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[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;assume A2: S

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

for n being Nat holds S

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