set a = the Element of S;
set s = <* the Element of S*>;
reconsider p = FDprobSEQ <* the Element of S*> as ProbFinS FinSequence of REAL by Th21;
dom p = Seg (card S) by Def3;
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