:: deftheorem Def4 defines `| PDIFF_9:def 4 :
for m being non zero Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL st Z c= dom f holds
for b<sub>4</sub> being PartFunc of (REAL m),(Funcs ((REAL m),REAL)) holds
( b<sub>4</sub> = f `| Z iff ( dom b₄ = Z & ( for x being Element of REAL m st x in Z holds
b₄ /. x = diff (f,x) ) ) );