set F = f1 / f2;
rng (f1 / f2) c= REAL by VALUED_0:def 3;
then f1 / f2 is PartFunc of dom (f1 / f2), REAL by RELSET_1:11;
hence f1 / f2 is PartFunc of C, REAL by RELSET_1:13; :: thesis: verum