:: deftheorem Def7 defines GenProbSEQ DIST_1:def 7 :
for S being finite set
for b₂ being Function of (distribution_family S),(REAL *) holds
( b₂ = GenProbSEQ S iff for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & b₂ . x = FDprobSEQ s ) );