:: deftheorem Def1 defines nonnegative ENTROPY1:def 1 :
for p being FinSequence of REAL holds
( p is nonnegative iff for i being Nat st i in dom p holds
p . i >= 0 );