theorem Th32: :: TAYLOR_1:32

for f being 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