:: deftheorem defines uniformly_distributed DIST_1:def 11 :
for S being finite set
for s being FinSequence of S holds
( s is uniformly_distributed iff for n being Nat st n in dom (FDprobSEQ s) holds
(FDprobSEQ s) . n = 1 / (card S) );