let S be finite set ; :: thesis: for s, t being FinSequence of S st s is uniformly_distributed & t is uniformly_distributed holds
s,t -are_prob_equivalent
let s, t be FinSequence of S; :: thesis: ( s is uniformly_distributed & t is uniformly_distributed implies s,t -are_prob_equivalent )
assume that
A1: s is uniformly_distributed and
A2: t is uniformly_distributed ; :: thesis: s,t -are_prob_equivalent
A3: ( dom (FDprobSEQ s) = Seg (card S) & dom (FDprobSEQ t) = Seg (card S) ) by Def3;
for n being object st n in dom (FDprobSEQ s) holds
(FDprobSEQ s) . n = (FDprobSEQ t) . n

proof

let n be object ; :: thesis: ( n in dom (FDprobSEQ s) implies (FDprobSEQ s) . n = (FDprobSEQ t) . n )
assume A4: n in dom (FDprobSEQ s) ; :: thesis: (FDprobSEQ s) . n = (FDprobSEQ t) . n
then (FDprobSEQ s) . n = 1 / (card S) by A1;
hence (FDprobSEQ s) . n = (FDprobSEQ t) . n by A2, A3, A4; :: thesis: verum

end;

then FDprobSEQ s = FDprobSEQ t by A3;
hence s,t -are_prob_equivalent by Th8; :: thesis: verum