theorem
Th17
:
:: DIST_1:19
for
S
being non
empty
finite
set
for
s
being non
empty
FinSequence
of
S
holds
Sum
(
FDprobSEQ
s
)
=
1