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

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