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 that
A1: Y c= rng f and
A2: f " Y is finite ; :: thesis: Y is finite
f .: (f " Y) = Y by A1, FUNCT_1:147;
hence Y is finite by A2; :: thesis: verum