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

hence s,t -are_prob_equivalent by Th8; :: thesis: verum

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

then
FDprobSEQ s = FDprobSEQ t
by A3;
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;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

hence s,t -are_prob_equivalent by Th8; :: thesis: verum