let S be 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
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, Th21;
hence t in Finseq-EQclass s ; :: thesis: verum