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: canFS S is_uniformly_distributed by Th26;
A2: 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 A1, Th25;
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, Lm2;
then A3: Finseq-EQclass (canFS S) = uniform_distribution S by A2, Def12;
(GenProbSEQ S) . (Finseq-EQclass (canFS S)) = Uniform_FDprobSEQ S by Th12;
then A4: (GenProbSEQ S) . (distribution ((Uniform_FDprobSEQ S),S)) = (GenProbSEQ S) . (Finseq-EQclass (canFS S)) by Th22;
dom (GenProbSEQ S) = distribution_family S by FUNCT_2:def 1;
hence uniform_distribution S = distribution ((Uniform_FDprobSEQ S),S) by A3, A4, FUNCT_1:def 8; :: thesis: verum