:: deftheorem defines #occurrences MMLQUERY:def 22 :
for A being FinSequence
for a being object holds #occurrences (a,A) = card { i where i is Element of NAT : ( i in dom A & a in A . i ) } ;