let x, X, Y be set ; :: thesis: for f being Function holds
( x in dom <:f,X,Y:> iff ( x in dom f & x in X & f . x in Y ) )
let f be Function; :: thesis: ( x in dom <:f,X,Y:> iff ( x in dom f & x in X & f . x in Y ) )
thus ( x in dom <:f,X,Y:> implies ( x in dom f & x in X & f . x in Y ) ) :: thesis: ( x in dom f & x in X & f . x in Y implies x in dom <:f,X,Y:> )

proof

assume x in dom <:f,X,Y:> ; :: thesis: ( x in dom f & x in X & f . x in Y )
then x in (dom (Y | f)) /\ X by RELAT_1:90;
then ( x in X & x in dom (Y | f) ) by XBOOLE_0:def 4;
hence ( x in dom f & x in X & f . x in Y ) by FUNCT_1:86; :: thesis: verum

end;

assume ( x in dom f & x in X & f . x in Y ) ; :: thesis: x in dom <:f,X,Y:>
then ( x in X & x in dom (Y | f) ) by FUNCT_1:86;
then x in (dom (Y | f)) /\ X by XBOOLE_0:def 4;
hence x in dom <:f,X,Y:> by RELAT_1:90; :: thesis: verum