let S be finite set ; :: thesis: for s, t being FinSequence of S st s is uniformly_distributed & s,t -are_prob_equivalent holds

t is uniformly_distributed

let s, t be FinSequence of S; :: thesis: ( s is uniformly_distributed & s,t -are_prob_equivalent implies t is uniformly_distributed )

assume that

A1: s is uniformly_distributed and

A2: s,t -are_prob_equivalent ; :: thesis: t is uniformly_distributed

FDprobSEQ s = FDprobSEQ t by A2, Th8;

then for n being Nat st n in dom (FDprobSEQ t) holds

(FDprobSEQ t) . n = 1 / (card S) by A1;

hence t is uniformly_distributed ; :: thesis: verum

t is uniformly_distributed

let s, t be FinSequence of S; :: thesis: ( s is uniformly_distributed & s,t -are_prob_equivalent implies t is uniformly_distributed )

assume that

A1: s is uniformly_distributed and

A2: s,t -are_prob_equivalent ; :: thesis: t is uniformly_distributed

FDprobSEQ s = FDprobSEQ t by A2, Th8;

then for n being Nat st n in dom (FDprobSEQ t) holds

(FDprobSEQ t) . n = 1 / (card S) by A1;

hence t is uniformly_distributed ; :: thesis: verum