:: deftheorem Def4 defines Vec2DiagMx ENTROPY1:def 4 :
for p being FinSequence of REAL
for b₂ being diagonal Matrix of len p,REAL holds
( b₂ = Vec2DiagMx p iff for j being Nat st j in dom p holds
b₂ * (j,j) = p . j );