theorem Th30: :: MATRIXR1:30

for a being Real
for A being Matrix of REAL st width A > 0 holds
(a * A) @ = a * (A @)