:: deftheorem defines frequency DIST_1:def 1 :
for S being finite set
for s being FinSequence of S
for x being set holds frequency (x,s) = card (event_pick (x,s));