for f being Function st dom f is finite holds
rng f is finite