:: deftheorem Def6 defines number_of MMLQUER2:def 6 :
for X being finite set
for O being Operation of X
for b₃ being Function of X,NAT holds
( b₃ = number_of O iff for x being Element of X holds b₃ . x = card (x . O) );