theorem :: FUNCT_2:41

for X, Y being set
for f being Function of X,Y holds
( ( for y being object st y in Y holds
f " {y} <> {} ) iff rng f = Y ) by FUNCT_1:73, FUNCT_1:72;