:: deftheorem Def10 defines distProbFinS DIST_1:def 10 :
for S being non empty finite set
for b₂ being ProbFinS FinSequence of REAL holds
( b₂ is distProbFinS of S iff ( len b₂ = card S & ex s being FinSequence of S st FDprobSEQ s = b₂ ) );