let X be set ; :: thesis: ( X = f " Y iff for x being object holds
( x in X iff ( x in dom f & f . x in Y ) ) )

hereby :: thesis: ( ( for x being object holds
( x in X iff ( x in dom f & f . x in Y ) ) ) implies X = f " Y )

assume A1: X = f " Y ; :: thesis: for x being object holds
( ( x in X implies ( x in dom f & f . x in Y ) ) & ( x in dom f & f . x in Y implies x in X ) )
let x be object ; :: thesis: ( ( x in X implies ( x in dom f & f . x in Y ) ) & ( x in dom f & f . x in Y implies x in X ) )

hereby :: thesis: ( x in dom f & f . x in Y implies x in X )

assume x in X ; :: thesis: ( x in dom f & f . x in Y )
then A2: ex y being object st
( [x,y] in f & y in Y ) by A1, RELAT_1:def 14;
hence x in dom f by XTUPLE_0:def 12; :: thesis: f . x in Y
thus f . x in Y by A2, Th1; :: thesis: verum

end;

assume that
A3: x in dom f and
A4: f . x in Y ; :: thesis: x in X
[x,(f . x)] in f by A3, Th1;
hence x in X by A1, A4, RELAT_1:def 14; :: thesis: verum

end;

assume A5: for x being object holds
( x in X iff ( x in dom f & f . x in Y ) ) ; :: thesis: X = f " Y

now :: thesis: for x being object holds
( ( x in X implies ex y being object st
( [x,y] in f & y in Y ) ) & ( ex y being object st
( [x,y] in f & y in Y ) implies x in X ) )

let x be object ; :: thesis: ( ( x in X implies ex y being object st
( [x,y] in f & y in Y ) ) & ( ex y being object st
( [x,y] in f & y in Y ) implies x in X ) )

hereby :: thesis: ( ex y being object st
( [x,y] in f & y in Y ) implies x in X )

assume A6: x in X ; :: thesis: ex y being object st
( [x,y] in f & y in Y )
reconsider y = f . x as object ;
take y = y; :: thesis: ( [x,y] in f & y in Y )
x in dom f by A5, A6;
hence [x,y] in f by Def2; :: thesis: y in Y
thus y in Y by A5, A6; :: thesis: verum

end;

given y being object such that A7: [x,y] in f and
A8: y in Y ; :: thesis: x in X
( x in dom f & y = f . x ) by A7, Th1;
hence x in X by A5, A8; :: thesis: verum

end;

hence X = f " Y by RELAT_1:def 14; :: thesis: verum