:: deftheorem Def1 defines / CFUNCT_1:def 1 :
for C being non empty set
for f1, f2, b₄ being PartFunc of C,COMPLEX holds
( b₄ = f1 / f2 iff ( dom b₄ = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom b₄ holds
b₄ /. c = (f1 /. c) * ((f2 /. c) ") ) ) );