thus dom (f +* x,y) = dom f by FUNCT_7:32
.= X by PBOOLE:def 3 ; :: according to PBOOLE:def 3 :: thesis: verum