theorem Th54: :: ENTROPY1:54

for M being m-nonnegative Matrix of REAL
for M1 being Matrix of REAL holds
( M1 = Infor_FinSeq_of M iff ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = (M * (i,j)) * (log (2,(M * (i,j)))) ) ) )