theorem
Th13
:
:: DIST_1:15
for
S
being
finite
set
for
s
being
FinSequence
of
S
holds
Sum
(
freqSEQ
s
)
=
(
len
s
)
*
(
Sum
(
FDprobSEQ
s
)
)