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 A1: 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 dom (Y | f) by XBOOLE_0:def 4;
hence ( x in dom f & x in X & f . x in Y ) by A1, FUNCT_1:86; :: thesis: verum

end;

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