:: deftheorem Def8 defines distribution DIST_1:def 8 :
for S being finite set
for p being ProbFinS FinSequence of REAL st ex s being FinSequence of S st FDprobSEQ s = p holds
for b₃ being Element of distribution_family S holds
( b₃ = distribution (p,S) iff (GenProbSEQ S) . b₃ = p );