let S be non empty finite set ; :: thesis: for D being EqSampleSpaces of S holds (GenProbSEQ S) . D is distProbFinS of S
let D be well-distributed Element of distribution_family S; :: thesis: (GenProbSEQ S) . D is distProbFinS of S
set s = the Element of D;
reconsider p = FDprobSEQ the Element of D as ProbFinS FinSequence of REAL ;
dom p = Seg (card S) by DIST_1:def 3;
then len p = card S by FINSEQ_1:def 3;
then A1: p is distProbFinS of S by DIST_1:def 10;
consider t being FinSequence of S such that
A2: D = Finseq-EQclass t by DIST_1:def 6;
D = Finseq-EQclass the Element of D by A2, DIST_1:9, DIST_1:7;
hence (GenProbSEQ S) . D is distProbFinS of S by A1, DIST_1:12; :: thesis: verum