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 S1[ Nat] means f . x = (Partial_Sums (Taylor (f,Z,x,x))) . \$1;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[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
.= (f . x) + (((((diff (f,Z)) . (k + 1)) . x) * ((0 |^ k) * 0)) / ((k + 1) !)) by NEWTON:6
.= f . x ; :: thesis: verum
end;
(Partial_Sums (Taylor (f,Z,x,x))) . 0 = (Taylor (f,Z,x,x)) . 0 by SERIES_1:def 1
.= ((((diff (f,Z)) . 0) . x) * ((x - x) |^ 0)) / () by Def7
.= (((f | Z) . x) * ((x - x) |^ 0)) / () by Def5
.= (((f | Z) . x) * 1) / 1 by
.= f . x by ;
then A4: S1[ 0 ] ;
for k being Nat holds S1[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