theorem Th23: :: MATRTOP1:23

for n, m being Nat
for r being Real
for f being b₁ -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)