theorem :: CARD_2:101

for F being Function st dom F is infinite & rng F is finite holds
ex x being object st
( x in rng F & F " {x} is infinite )