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
L3: CS = Finseq-EQclass (canFS S) ;
reconsider CS = CS as Element of distribution_family S by defQuot, L3;
assume s in Finseq-EQclass (canFS S) ; :: thesis: s is_uniformly_distributed
then s, canFS S -are_prob_equivalent by EQX02;
hence s is_uniformly_distributed by THUDEQ, THUDS; :: thesis: verum