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