:: deftheorem defines Uniform_FDprobSEQ DIST_1:def 13 :
for S being non empty finite set holds Uniform_FDprobSEQ S = FDprobSEQ (canFS S);