dom (f " ) = dom f by Def7
.= C by FUNCT_2:def 1 ;
hence f " is total PartFunc of C, RAT by PARTFUN1:def 4; :: thesis: verum