:: deftheorem Def1 defines Cardinal-yielding CARD_3:def 1 :
for IT being Function holds
( IT is Cardinal-yielding iff for x being object st x in dom IT holds
IT . x is Cardinal );