theorem Th10: :: FINSET_1:10

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