reconsider s = canFS S as Element of S * by FINSEQ_1:def 11;
take p = FDprobSEQ s; :: thesis: ( p is distProbFinS of S & p is constant )
dom p = Seg (card S) by Def3;
then len p = card S by FINSEQ_1:def 3;
hence ( p is distProbFinS of S & p is constant ) by Def10, Th19; :: thesis: verum