dom (f1 /" f2) = C by Lm4;
hence f1 /" f2 is total PartFunc of C, REAL by PARTFUN1:def 4; :: thesis: verum