consider a being Element of S;
set s = <*a*>;
reconsider p = FDprobSEQ <*a*> as ProbFinS FinSequence of REAL by FREQDISTSUM2;
dom p = Seg (card S) by defFREQDIST;
then len p = card S by FINSEQ_1:def 3;
hence ex b₁ being ProbFinS FinSequence of REAL st
( len b₁ = card S & ex s being FinSequence of S st FDprobSEQ s = b₁ ) ; :: thesis: verum