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