for f being Function holds
( dom f is finite iff f is finite )