theorem Th48: :: ENTROPY1:48

for p being nonnegative FinSequence of REAL
for k being Nat st k in dom p holds
( ( p . k = 0 implies (Infor_FinSeq_of p) . k = 0 ) & ( p . k > 0 implies (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) ) )