:: deftheorem Def7 defines Taylor TAYLOR_1:def 7 :
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for a, b being Real
for b₅ being Real_Sequence holds
( b₅ = Taylor (f,Z,a,b) iff for n being Nat holds b₅ . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) );