theorem :: MATRLIN2:38

for K being Field
for a being Element of K
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for A being Matrix of len b1, len B2,K holds a * (Mx2Tran (A,b1,B2)) = Mx2Tran ((a * A),b1,B2)