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