let f be PartFunc of REAL,REAL; 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; 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; ( x in Z implies for n being Nat holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n )
assume A1:
x in Z
; 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;
( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
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 A3, Def7
.=
(f . x) + (((((diff (f,Z)) . (k + 1)) . x) * ((0 |^ k) * 0)) / ((k + 1) !))
by NEWTON:6
.=
f . x
;
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)) / (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:
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
; verum