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