:: deftheorem Def8 defines count_reps POLYNOM9:def 8 :
for n being Nat
for f being finite Function
for b₃ being bag of n holds
( b₃ = count_reps (f,n) iff for i being Nat st i in n holds
b₃ . i = card (f " {(i + 1)}) );