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