let S be non empty 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 set st n in dom (FDprobSEQ s) holds
(FDprobSEQ s) . n = (FDprobSEQ t) . n

proof

let n be set ; :: 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, Def11;
hence (FDprobSEQ s) . n = (FDprobSEQ t) . n by A2, A3, A4, Def11; :: thesis: verum

end;

then FDprobSEQ s = FDprobSEQ t by A3, FUNCT_1:2;
hence s,t -are_prob_equivalent by Th10; :: thesis: verum