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;
ES1: canFS S is_uniformly_distributed by THUDS;
ZZ0: (GenProbSEQ S) . (Finseq-EQclass (canFS S)) = Uniform_FDprobSEQ S by EQX07;
ZZ1: for t being FinSequence of S st t in Finseq-EQclass (canFS S) holds
t is_uniformly_distributed by THCFS;
nazo: Finseq-EQclass (canFS S) is Element of distribution_family S by defQuot;
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 THUDEQ2, ES1;
hence t in Finseq-EQclass (canFS S) ; :: thesis: verum

end;

then T1: Finseq-EQclass (canFS S) = uniform_distribution S by ZZ1, defunidist, nazo;
ZZ02: (GenProbSEQ S) . (distribution (Uniform_FDprobSEQ S),S) = (GenProbSEQ S) . (Finseq-EQclass (canFS S)) by ZZ0, pbf;
dom (GenProbSEQ S) = distribution_family S by FUNCT_2:def 1;
hence uniform_distribution S = distribution (Uniform_FDprobSEQ S),S by ZZ02, T1, FUNCT_1:def 8; :: thesis: verum