dom (f +* (x,y)) = dom f by FUNCT_7:32
.= X by PARTFUN1:def 4 ;
hence f +* (x,y) is X -defined by RELAT_1:def 18; :: thesis: verum