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