let P be PFUNC_DOMAIN of X,Y; :: thesis: P is functional
let x be set ; :: according to FUNCT_1:def 19 :: thesis: ( not x in P or x is set )
assume x in P ; :: thesis: x is set
hence x is set by RFUNCT_3:def 3; :: thesis: verum