theorem :: DIST_1:24

for S being non empty finite set holds uniform_distribution S = distribution ((Uniform_FDprobSEQ S),S)