theorem Th5: :: DIST_2:5

for S being non empty finite set
for s being FinSequence of S holds
( ( for x being set holds FDprobability (x,s) = 0 ) iff s is empty )