theorem Th42: :: MATRIX10:42

for a being Real
for n being Nat
for M being Matrix of n,REAL st a >= 0 & M is Nonnegative holds
a * M is Nonnegative