:: deftheorem Def5 defines diff TAYLOR_1:def 5 :
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for b₃ being Functional_Sequence of REAL,REAL holds
( b₃ = diff (f,Z) iff ( b₃ . 0 = f | Z & ( for i being Nat holds b₃ . (i + 1) = (b₃ . i) `| Z ) ) );