theorem Th56: :: MATRIXR1:56

for a being Real
for M being Matrix of REAL
for i being Nat st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))