:: deftheorem Def1 defines finite FINSET_1:def 1 :
for IT being set holds
( IT is finite iff ex p being Function st
( rng p = IT & dom p in omega ) );