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