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