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