let Y be set ; :: thesis: ( Y = rng f iff for y being object holds
( y in Y iff ex x being object st
( x in dom f & y = f . x ) ) )
hereby :: thesis: ( ( for y being object holds
( y in Y iff ex x being object st
( x in dom f & y = f . x ) ) ) implies Y = rng f )
assume A1: Y = rng f ; :: thesis: for y being object holds
( ( y in Y implies ex x being object st
( x in dom f & y = f . x ) ) & ( ex x being object st
( x in dom f & 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 & y = f . x ) ) & ( ex x being object st
( x in dom f & y = f . x ) implies y in Y ) )
hereby :: thesis: ( ex x being object st
( x in dom f & y = f . x ) implies y in Y )
assume y in Y ; :: thesis: ex x being object st
( x in dom f & y = f . x )
then consider x being object such that
A2: [x,y] in f by A1, XTUPLE_0:def 13;
take x = x; :: thesis: ( x in dom f & y = f . x )
thus ( x in dom f & y = f . x ) by A2, Th1; :: thesis: verum
end;
given x being object such that A3: ( x in dom f & y = f . x ) ; :: thesis: y in Y
[x,y] in f by A3, Def2;
hence y in Y by A1, XTUPLE_0:def 13; :: thesis: verum
end;
assume A4: for y being object holds
( y in Y iff ex x being object 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 object ; :: thesis: ( y in Y implies y in rng f )
assume y in Y ; :: thesis: y in rng f
then consider x being object such that
A5: ( x in dom f & y = f . x ) by A4;
[x,y] in f by A5, Def2;
hence y in rng f by XTUPLE_0:def 13; :: thesis: verum
end;
let y be object ; :: 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 object such that
A6: [x,y] in f by XTUPLE_0:def 13;
( x in dom f & y = f . x ) by A6, Th1;
hence y in Y by A4; :: thesis: verum