let S be non empty finite set ; :: thesis: for s being FinSequence of S st s is_uniformly_distributed holds
for t being FinSequence of S st t is_uniformly_distributed holds
t in Finseq-EQclass s
let s be FinSequence of S; :: thesis: ( s is_uniformly_distributed implies for t being FinSequence of S st t is_uniformly_distributed holds
t in Finseq-EQclass s )
assume A1: s is_uniformly_distributed ; :: thesis: for t being FinSequence of S st t is_uniformly_distributed holds
t in Finseq-EQclass s
for t being FinSequence of S st t is_uniformly_distributed holds
t in Finseq-EQclass s

proof

let t be FinSequence of S; :: thesis: ( t is_uniformly_distributed implies t in Finseq-EQclass s )
assume t is_uniformly_distributed ; :: thesis: t in Finseq-EQclass s
then s,t -are_prob_equivalent by A1, Th25;
hence t in Finseq-EQclass s ; :: thesis: verum

end;

hence for t being FinSequence of S st t is_uniformly_distributed holds
t in Finseq-EQclass s ; :: thesis: verum