let S be finite set ; :: thesis: for s being FinSequence of S st s in Finseq-EQclass (canFS S) holds
s is uniformly_distributed
let s be FinSequence of S; :: thesis: ( s in Finseq-EQclass (canFS S) implies s is uniformly_distributed )
assume s in Finseq-EQclass (canFS S) ; :: thesis: s is uniformly_distributed
then s, canFS S -are_prob_equivalent by Th7;
hence s is uniformly_distributed by Th24; :: thesis: verum