theorem Th26: :: ENTROPY1:26

for p being FinSequence of REAL
for MR, MR1 being Matrix of REAL st len p = len MR holds
( MR1 = (Vec2DiagMx p) * MR iff ( len MR1 = len p & width MR1 = width MR & ( for i, j being Nat st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j)) ) ) )