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 )
consider CS being non empty Subset of (S * ) such that
A1: CS = Finseq-EQclass (canFS S) ;
reconsider CS = CS as Element of distribution_family S by A1, Def6;
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