let S be non empty finite set ; :: thesis: for s being non empty FinSequence of S holds Sum (FDprobSEQ s) = 1
let s be non empty FinSequence of S; :: thesis: Sum (FDprobSEQ s) = 1
Sum (freqSEQ s) = len s by Th16;
then (len s) * (Sum (FDprobSEQ s)) = (len s) * 1 by Th13;
hence Sum (FDprobSEQ s) = 1 by XCMPLX_1:5; :: thesis: verum