let S be non empty 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, Th10;
then for n being Nat st n in dom (FDprobSEQ t) holds
(FDprobSEQ t) . n = 1 / (card S) by A1, Def11;
hence t is_uniformly_distributed by Def11; :: thesis: verum