let a be Real; :: thesis: for s being Real_Sequence st ( for n being Nat st n >= 1 holds

( s . n = a / n & s . 0 = 1 ) ) holds

for n being Nat st n >= 1 holds

(Partial_Product s) . n = (a |^ n) / (n !)

let s be Real_Sequence; :: thesis: ( ( for n being Nat st n >= 1 holds

( s . n = a / n & s . 0 = 1 ) ) implies for n being Nat st n >= 1 holds

(Partial_Product s) . n = (a |^ n) / (n !) )

defpred S_{1}[ Nat] means (Partial_Product s) . $1 = (a |^ $1) / ($1 !);

assume A1: for n being Nat st n >= 1 holds

( s . n = a / n & s . 0 = 1 ) ; :: thesis: for n being Nat st n >= 1 holds

(Partial_Product s) . n = (a |^ n) / (n !)

A2: for n being Nat st n >= 1 & S_{1}[n] holds

S_{1}[n + 1]

.= (s . 0) * (s . (1 + 0)) by SERIES_3:def 1

.= 1 * (s . 1) by A1

.= (1 * a) / 1 by A1

.= (a |^ 1) / (1 !) by NEWTON:13 ;

then A5: S_{1}[1]
;

for n being Nat st n >= 1 holds

S_{1}[n]
from NAT_1:sch 8(A5, A2);

hence for n being Nat st n >= 1 holds

(Partial_Product s) . n = (a |^ n) / (n !) ; :: thesis: verum

( s . n = a / n & s . 0 = 1 ) ) holds

for n being Nat st n >= 1 holds

(Partial_Product s) . n = (a |^ n) / (n !)

let s be Real_Sequence; :: thesis: ( ( for n being Nat st n >= 1 holds

( s . n = a / n & s . 0 = 1 ) ) implies for n being Nat st n >= 1 holds

(Partial_Product s) . n = (a |^ n) / (n !) )

defpred S

assume A1: for n being Nat st n >= 1 holds

( s . n = a / n & s . 0 = 1 ) ; :: thesis: for n being Nat st n >= 1 holds

(Partial_Product s) . n = (a |^ n) / (n !)

A2: for n being Nat st n >= 1 & S

S

proof

(Partial_Product s) . (1 + 0) =
((Partial_Product s) . 0) * (s . (1 + 0))
by SERIES_3:def 1
let n be Nat; :: thesis: ( n >= 1 & S_{1}[n] implies S_{1}[n + 1] )

assume that

n >= 1 and

A3: (Partial_Product s) . n = (a |^ n) / (n !) ; :: thesis: S_{1}[n + 1]

A4: n + 1 >= 1 by NAT_1:11;

(Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by SERIES_3:def 1

.= ((a |^ n) / (n !)) * (a / (n + 1)) by A1, A3, A4

.= ((a |^ n) * a) / ((n !) * (n + 1)) by XCMPLX_1:76

.= (a |^ (n + 1)) / ((n !) * (n + 1)) by NEWTON:6

.= (a |^ (n + 1)) / ((n + 1) !) by NEWTON:15 ;

hence S_{1}[n + 1]
; :: thesis: verum

end;assume that

n >= 1 and

A3: (Partial_Product s) . n = (a |^ n) / (n !) ; :: thesis: S

A4: n + 1 >= 1 by NAT_1:11;

(Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by SERIES_3:def 1

.= ((a |^ n) / (n !)) * (a / (n + 1)) by A1, A3, A4

.= ((a |^ n) * a) / ((n !) * (n + 1)) by XCMPLX_1:76

.= (a |^ (n + 1)) / ((n !) * (n + 1)) by NEWTON:6

.= (a |^ (n + 1)) / ((n + 1) !) by NEWTON:15 ;

hence S

.= (s . 0) * (s . (1 + 0)) by SERIES_3:def 1

.= 1 * (s . 1) by A1

.= (1 * a) / 1 by A1

.= (a |^ 1) / (1 !) by NEWTON:13 ;

then A5: S

for n being Nat st n >= 1 holds

S

hence for n being Nat st n >= 1 holds

(Partial_Product s) . n = (a |^ n) / (n !) ; :: thesis: verum