:: deftheorem Def3 defines rng FUNCT_1:def 3 :
for f being Function
for b₂ being set holds
( b₂ = rng f iff for y being object holds
( y in b₂ iff ex x being object st
( x in dom f & y = f . x ) ) );