let X, Y be set ; :: thesis: for f being Function of X,Y st Y <> {} & ( for y being set st y in Y holds
ex x being set st
( x in X & y = f . x ) ) holds
rng f = Y
let f be Function of X,Y; :: thesis: ( Y <> {} & ( for y being set st y in Y holds
ex x being set st
( x in X & y = f . x ) ) implies rng f = Y )
assume that
A1: Y <> {} and
A2: for y being set st y in Y holds
ex x being set st
( x in X & y = f . x ) ; :: thesis: rng f = Y
for y being set holds
( y in rng f iff y in Y )

proof

let y be set ; :: thesis: ( y in rng f iff y in Y )
dom f = X by A1, Def1;
then ( ( y in rng f implies ex x being set st
( x in X & y = f . x ) ) & ( ex x being set st
( x in X & y = f . x ) implies y in rng f ) & rng f c= Y ) by FUNCT_1:def 5;
hence ( y in rng f iff y in Y ) by A2; :: thesis: verum

end;

hence rng f = Y by TARSKI:2; :: thesis: verum