theorem Th47: :: ENTROPY1:47

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,(p . k))) ) ) )