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

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