dom (r (#) f) = dom f by Def5
.= C by FUNCT_2:def 1 ;
hence r (#) f is total PartFunc of C, COMPLEX by PARTFUN1:def 4; :: thesis: verum