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

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

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

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

assume y in Y ; :: thesis: ex x being set st
( x in dom f & y = f . x )
then consider x being set such that
A2: [x,y] in f by A1, RELAT_1:def 5;
take x = x; :: thesis: ( x in dom f & y = f . x )
thus ( x in dom f & y = f . x ) by A2, Th8; :: thesis: verum

end;

given x being set such that A3: ( x in dom f & y = f . x ) ; :: thesis: y in Y
[x,y] in f by A3, Def4;
hence y in Y by A1, RELAT_1:def 5; :: thesis: verum

end;

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

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: rng f c= Y

let y be set ; :: thesis: ( y in Y implies y in rng f )
assume y in Y ; :: thesis: y in rng f
then consider x being set such that
A5: ( x in dom f & y = f . x ) by A4;
[x,y] in f by A5, Def4;
hence y in rng f by RELAT_1:def 5; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Y )
assume y in rng f ; :: thesis: y in Y
then consider x being set such that
A6: [x,y] in f by RELAT_1:def 5;
( x in dom f & y = f . x ) by A6, Th8;
hence y in Y by A4; :: thesis: verum