let f be Function; :: thesis: for Y being set holds dom (Y | f) = f " Y
let Y be set ; :: thesis: dom (Y | f) = f " Y
for x being set holds
( x in dom (Y | f) iff x in f " Y )

proof

let x be set ; :: thesis: ( x in dom (Y | f) iff x in f " Y )

hereby :: thesis: ( x in f " Y implies x in dom (Y | f) )

assume x in dom (Y | f) ; :: thesis: x in f " Y
then consider y being set such that
A1: [x,y] in Y | f by RELAT_1:def 4;
( y in Y & [x,y] in f ) by A1, RELAT_1:def 12;
hence x in f " Y by RELAT_1:def 14; :: thesis: verum

end;

assume x in f " Y ; :: thesis: x in dom (Y | f)
then consider y being set such that
A2: ( [x,y] in f & y in Y ) by RELAT_1:def 14;
[x,y] in Y | f by A2, RELAT_1:def 12;
hence x in dom (Y | f) by RELAT_1:def 4; :: thesis: verum

end;

hence dom (Y | f) = f " Y by TARSKI:1; :: thesis: verum