let X, Y be set ; :: thesis: for f being Function of X,Y holds
( ( for y being set st y in Y holds
f " {y} <> {} ) iff rng f = Y )
let f be Function of X,Y; :: thesis: ( ( for y being set st y in Y holds
f " {y} <> {} ) iff rng f = Y )
thus ( ( for y being set st y in Y holds
f " {y} <> {} ) implies rng f = Y ) :: thesis: ( rng f = Y implies for y being set st y in Y holds
f " {y} <> {} )

proof

assume for y being set st y in Y holds
f " {y} <> {} ; :: thesis: rng f = Y
then ( rng f c= Y & Y c= rng f ) by FUNCT_1:143;
hence rng f = Y by XBOOLE_0:def 10; :: thesis: verum

end;

thus ( rng f = Y implies for y being set st y in Y holds
f " {y} <> {} ) by FUNCT_1:142; :: thesis: verum