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 Element of 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 Element of NAT holds f . x = (Partial_Sums (Taylor f,Z,x,x)) . n
let x be Real; :: thesis: ( x in Z implies for n being Element of NAT holds f . x = (Partial_Sums (Taylor f,Z,x,x)) . n )
assume A1: x in Z ; :: thesis: for n being Element of NAT holds f . x = (Partial_Sums (Taylor f,Z,x,x)) . n
defpred S₁[ Element of NAT ] means f . x = (Partial_Sums (Taylor f,Z,x,x)) . $1;
A2: S₁[ 0 ]

proof

thus (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:9, NEWTON:18
.= f . x by A1, FUNCT_1:72 ; :: thesis: verum

end;

A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[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 A4, Def7
.= (f . x) + (((((diff f,Z) . (k + 1)) . x) * ((0 |^ k) * 0 )) / ((k + 1) ! )) by NEWTON:11
.= f . x ; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);
hence for n being Element of NAT holds f . x = (Partial_Sums (Taylor f,Z,x,x)) . n ; :: thesis: verum