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