for Y being set
for f being Function st Y c= rng f & f " Y is finite holds
Y is finite