thus dom (r (#) f) = dom f by Def4
.= C by FUNCT_2:def 1 ; :: according to PARTFUN1:def 2 :: thesis: verum