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)

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

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

( ( for t being FinSequence of S st t in Finseq-EQclass (canFS S) holds
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;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

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