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

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

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

hereby :: thesis: ( ex x being object st
( x in dom f & x in X & y = f . x ) implies y in Y )

assume y in Y ; :: thesis: ex x being object st
( x in dom f & x in X & y = f . x )
then consider x being object such that
A2: [x,y] in f and
A3: x in X by A1, RELAT_1:def 13;
reconsider x = x as object ;
take x = x; :: thesis: ( x in dom f & x in X & y = f . x )
thus A4: x in dom f by A2, XTUPLE_0:def 12; :: thesis: ( x in X & y = f . x )
reconsider yy = y as set by TARSKI:1;
thus x in X by A3; :: thesis: y = f . x
yy = f . x by A2, A4, Def2;
hence y = f . x ; :: thesis: verum

end;

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

end;

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

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

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

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

assume y in Y ; :: thesis: ex x being object st
( [x,y] in f & x in X )
then consider x being object such that
A9: x in dom f and
A10: x in X and
A11: y = f . x by A8;
reconsider x = x as object ;
take x = x; :: thesis: ( [x,y] in f & x in X )
thus [x,y] in f by A9, A11, Def2; :: thesis: x in X
thus x in X by A10; :: thesis: verum

end;

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

end;

hence Y = f .: X by RELAT_1:def 13; :: thesis: verum