for p, q being non empty ProbFinS FinSequence of REAL
for pp, qq being FinSequence of REAL st len p = len q & len pp = len p & len qq = len q & ( for k being Nat st k in dom p holds
( p . k > 0 & q . k > 0 & pp . k = - ((p . k) * (log (2,(p . k)))) & qq . k = - ((p . k) * (log (2,(q . k)))) ) ) holds
( Sum pp <= Sum qq & ( ( for k being Nat st k in dom p holds
p . k = q . k ) implies Sum pp = Sum qq ) & ( Sum pp = Sum qq implies for k being Nat st k in dom p holds
p . k = q . k ) & ( ex k being Nat st
( k in dom p & p . k <> q . k ) implies Sum pp < Sum qq ) & ( Sum pp < Sum qq implies ex k being Nat st
( k in dom p & p . k <> q . k ) ) )