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 object holds
( x in dom (Y |` f) iff x in f " Y )

proof

let x be object ; :: 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 object such that
A1: [x,y] in Y |` f by XTUPLE_0:def 12;
( 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 object 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 XTUPLE_0:def 12; :: thesis: verum

end;

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