:: deftheorem Def9 defines freqSEQ DIST_1:def 9 :
for S being finite set
for s being FinSequence of S
for b₃ being FinSequence of NAT holds
( b₃ = freqSEQ s iff ( dom b₃ = Seg (card S) & ( for n being Nat st n in dom b₃ holds
b₃ . n = (len s) * ((FDprobSEQ s) . n) ) ) );