set F = f1 / f2;
A1: rng (f1 / f2) c= COMPLEX ;
dom (f1 / f2) = (dom f1) /\ ((dom f2) \ (f2 " {0})) by Def1;
hence f1 / f2 is PartFunc of C,COMPLEX by A1, RELSET_1:4; :: thesis: verum