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:4;
hence f1 / f2 is PartFunc of C,REAL by RELSET_1:5; :: thesis: verum