:: deftheorem Def12 defines uniform_distribution DIST_1:def 12 :
for S being finite set
for b₂ being Element of distribution_family S holds
( b₂ = uniform_distribution S iff for s being FinSequence of S holds
( s in b₂ iff s is uniformly_distributed ) );