theorem Th14: :: ENTROPY1:14

for p being FinSequence of REAL st p is nonnegative holds
for k being Nat st k in dom p & p . k = Sum p holds
p has_onlyone_value_in k