let X be set ; :: thesis:

hereby :: thesis:

assume A1: X = f " Y ; :: thesis:
let x be object ; :: thesis:

hereby :: thesis:

assume x in X ; :: thesis:
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:
thus f . x in Y by A2, Th1; :: thesis:

end;

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

end;

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

let x be object ; :: thesis:

hereby :: thesis:

assume A6: x in X ; :: thesis:
reconsider y = f . x as object ;
take y = y; :: thesis:
x in dom f by A5, A6;
hence [x,y] in f by Def2; :: thesis:
thus y in Y by A5, A6; :: thesis:

end;

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

end;

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