theorem Th27: :: ENTROPY1:27

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 being Nat st i in dom MR1 holds
Line (MR1,i) = (p . i) * (Line (MR,i)) ) ) )