:: deftheorem Def1 defines / RFUNCT_1:def 1 :
for f1, f2 being complex-valued Function
for b₃ being Function holds
( b₃ = f1 / f2 iff ( dom b₃ = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being object st c in dom b₃ holds
b₃ . c = (f1 . c) * ((f2 . c) ") ) ) );