theorem :: ENTROPY1:49

for p being nonnegative FinSequence of REAL
for q being FinSequence of REAL holds
( q = - (Infor_FinSeq_of p) iff ( len q = len p & ( for k being Nat st k in dom q holds
q . k = (p . k) * (log (2,(1 / (p . k)))) ) ) )