theorem Th15: :: ENTROPY1:15

for p being ProbFinS FinSequence of REAL
for k being Nat st k in dom p & p . k = 1 holds
p has_onlyone_value_in k