for p being non empty ProbFinS FinSequence of REAL st ( for k being Nat st k in dom p holds
p . k > 0 ) holds
( Entropy p <= log (2,(len p)) & ( ( for k being Nat st k in dom p holds
p . k = 1 / (len p) ) implies Entropy p = log (2,(len p)) ) & ( Entropy p = log (2,(len p)) implies for k being Nat st k in dom p holds
p . k = 1 / (len p) ) & ( ex k being Nat st
( k in dom p & p . k <> 1 / (len p) ) implies Entropy p < log (2,(len p)) ) & ( Entropy p < log (2,(len p)) implies ex k being Nat st
( k in dom p & p . k <> 1 / (len p) ) ) )