let S be non empty 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, Th26; :: thesis: verum