:: deftheorem Def4 defines `| NDIFF_4:def 4 :
for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n)
for X being set st f is_differentiable_on X holds
for b<sub>4</sub> being PartFunc of REAL,(REAL n) holds
( b<sub>4</sub> = f `| X iff ( dom b₄ = X & ( for x being Real st x in X holds
b₄ . x = diff (f,x) ) ) );