set a = the Element of S;
set s = <* the Element of S*>;
set p = FDprobSEQ <* the Element of S*>;
dom (FDprobSEQ <* the Element of S*>) = Seg (card S) by Def3;
then len (FDprobSEQ <* the Element of S*>) = 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