for p being non empty ProbFinS FinSequence of REAL st ex k being Nat st
( k in dom p & p . k = 1 ) holds
Entropy p = 0