:: deftheorem defines has_onlyone_value_in ENTROPY1:def 2 :
for p being FinSequence of REAL
for k being Nat holds
( p has_onlyone_value_in k iff ( k in dom p & ( for i being Nat st i in dom p & i <> k holds
p . i = 0 ) ) );