:: deftheorem Def8 defines Infor_FinSeq_of ENTROPY1:def 8 :
for MR being Matrix of REAL st MR is m-nonnegative holds
for b₂ being Matrix of REAL holds
( b₂ = Infor_FinSeq_of MR iff ( len b₂ = len MR & width b₂ = width MR & ( for k being Nat st k in dom b₂ holds
b₂ . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) ) );