let f be PartFunc of REAL,REAL; :: thesis: for Z being Subset of REAL

for x being Real st x in Z holds

for n being Nat holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n

let Z be Subset of REAL; :: thesis: for x being Real st x in Z holds

for n being Nat holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n

let x be Real; :: thesis: ( x in Z implies for n being Nat holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n )

assume A1: x in Z ; :: thesis: for n being Nat holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n

defpred S_{1}[ Nat] means f . x = (Partial_Sums (Taylor (f,Z,x,x))) . $1;

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

S_{1}[k + 1]

.= ((((diff (f,Z)) . 0) . x) * ((x - x) |^ 0)) / (0 !) by Def7

.= (((f | Z) . x) * ((x - x) |^ 0)) / (0 !) by Def5

.= (((f | Z) . x) * 1) / 1 by NEWTON:4, NEWTON:12

.= f . x by A1, FUNCT_1:49 ;

then A4: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A4, A2);

hence for n being Nat holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n ; :: thesis: verum

for x being Real st x in Z holds

for n being Nat holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n

let Z be Subset of REAL; :: thesis: for x being Real st x in Z holds

for n being Nat holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n

let x be Real; :: thesis: ( x in Z implies for n being Nat holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n )

assume A1: x in Z ; :: thesis: for n being Nat holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n

defpred S

A2: for k being Nat st S

S

proof

(Partial_Sums (Taylor (f,Z,x,x))) . 0 =
(Taylor (f,Z,x,x)) . 0
by SERIES_1:def 1
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

thus (Partial_Sums (Taylor (f,Z,x,x))) . (k + 1) = ((Partial_Sums (Taylor (f,Z,x,x))) . k) + ((Taylor (f,Z,x,x)) . (k + 1)) by SERIES_1:def 1

.= (f . x) + (((((diff (f,Z)) . (k + 1)) . x) * ((x - x) |^ (k + 1))) / ((k + 1) !)) by A3, Def7

.= (f . x) + (((((diff (f,Z)) . (k + 1)) . x) * ((0 |^ k) * 0)) / ((k + 1) !)) by NEWTON:6

.= f . x ; :: thesis: verum

end;assume A3: S

thus (Partial_Sums (Taylor (f,Z,x,x))) . (k + 1) = ((Partial_Sums (Taylor (f,Z,x,x))) . k) + ((Taylor (f,Z,x,x)) . (k + 1)) by SERIES_1:def 1

.= (f . x) + (((((diff (f,Z)) . (k + 1)) . x) * ((x - x) |^ (k + 1))) / ((k + 1) !)) by A3, Def7

.= (f . x) + (((((diff (f,Z)) . (k + 1)) . x) * ((0 |^ k) * 0)) / ((k + 1) !)) by NEWTON:6

.= f . x ; :: thesis: verum

.= ((((diff (f,Z)) . 0) . x) * ((x - x) |^ 0)) / (0 !) by Def7

.= (((f | Z) . x) * ((x - x) |^ 0)) / (0 !) by Def5

.= (((f | Z) . x) * 1) / 1 by NEWTON:4, NEWTON:12

.= f . x by A1, FUNCT_1:49 ;

then A4: S

for k being Nat holds S

hence for n being Nat holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n ; :: thesis: verum