theorem :: FUNCT_2:10

for X, Y being set
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