:: deftheorem Def2 defines Card CARD_3:def 2 :
for f being Function
for b₂ being Cardinal-Function holds
( b₂ = Card f iff ( dom b₂ = dom f & ( for x being object st x in dom f holds
b₂ . x = card (f . x) ) ) );