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

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