:: deftheorem Def12 defines `| CFDIFF_1:def 12 :
for f being PartFunc of COMPLEX,COMPLEX
for X being set st f is_differentiable_on X holds
for b<sub>3</sub> being PartFunc of COMPLEX,COMPLEX holds
( b<sub>3</sub> = f `| X iff ( dom b₃ = X & ( for x being Complex st x in X holds
b₃ /. x = diff (f,x) ) ) );