let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in rng f or x is set )
assume x in rng f ; :: thesis: x is set
then ex y being object st
( y in dom f & x = f . y ) by FUNCT_1:def 3;
hence x is set ; :: thesis: verum