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

per cases ( Y = {} or Y <> {} ) ;

suppose Y = {} ; :: thesis: rng f = Y

hence rng f = Y ; :: thesis: verum

end;

suppose A2: Y <> {} ; :: thesis: rng f = Y

for y being object holds
( y in rng f iff y in Y )

proof

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

end;

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

end;

end;