let S be non empty finite set ; :: thesis: uniform_distribution S = distribution ((Uniform_FDprobSEQ S),S)
set p = Uniform_FDprobSEQ S;
set s = canFS S;
A1: for t being FinSequence of S st t is uniformly_distributed holds
t in Finseq-EQclass (canFS S)

proof

let t be FinSequence of S; :: thesis: ( t is uniformly_distributed implies t in Finseq-EQclass (canFS S) )
assume t is uniformly_distributed ; :: thesis: t in Finseq-EQclass (canFS S)
then canFS S,t -are_prob_equivalent by Th21;
hence t in Finseq-EQclass (canFS S) ; :: thesis: verum

end;

( ( for t being FinSequence of S st t in Finseq-EQclass (canFS S) holds
t is uniformly_distributed ) & Finseq-EQclass (canFS S) is Element of distribution_family S ) by Def6, Lm3;
then A2: Finseq-EQclass (canFS S) = uniform_distribution S by A1, Def12;
(GenProbSEQ S) . (Finseq-EQclass (canFS S)) = Uniform_FDprobSEQ S by Th10;
then A3: (GenProbSEQ S) . (distribution ((Uniform_FDprobSEQ S),S)) = (GenProbSEQ S) . (Finseq-EQclass (canFS S)) by Th18;
dom (GenProbSEQ S) = distribution_family S by FUNCT_2:def 1;
hence uniform_distribution S = distribution ((Uniform_FDprobSEQ S),S) by A2, A3, FUNCT_1:def 4; :: thesis: verum