let Y be set ; :: thesis: for f being Function st Y c= rng f & f " Y is finite holds
Y is finite
let f be Function; :: thesis: ( Y c= rng f & f " Y is finite implies Y is finite )
assume Y c= rng f ; :: thesis: ( not f " Y is finite or Y is finite )
then f .: (f " Y) = Y by FUNCT_1:77;
hence ( not f " Y is finite or Y is finite ) ; :: thesis: verum