end;

given x being set such that A5: x in dom f and
A6: x in X and
A7: y = f . x ; :: thesis:
[x,y] in f by A5, A7, Def4;
hence y in Y by A1, A6, RELAT_1:def 13; :: thesis:

end;

assume A8: for y being set holds
( y in Y iff ex x being set st
( x in dom f & x in X & y = f . x ) ) ; :: thesis:

let y be set ; :: thesis:

assume y in Y ; :: thesis:
then consider x being set such that
A9: x in dom f and
A10: x in X and
A11: y = f . x by A8;
take x = x; :: thesis:
thus [x,y] in f by A9, A11, Def4; :: thesis:
thus x in X by A10; :: thesis:

end;

given x being set such that A12: [x,y] in f and
A13: x in X ; :: thesis:
( x in dom f & y = f . x ) by A12, Th8;
hence y in Y by A8, A13; :: thesis:

end;