consider s being FinSequence of S such that
A1: s = canFS S ;
reconsider s = s as Element of S * by FINSEQ_1:def 11;
consider p being FinSequence of REAL such that
A2: p = FDprobSEQ s ;
take p ; :: thesis: ( p is distProbFinS of S & p is constant )
dom p = Seg (card S) by A2, Def3;
then A3: len p = card S by FINSEQ_1:def 3;
( p is constant & p is ProbFinS ) by A1, A2, Th21, Th23, Th26;
hence ( p is distProbFinS of S & p is constant ) by A2, A3, Def10; :: thesis: verum