theorem Th32: :: MATRLIN2:32

for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for M being Matrix of len b1, len b2,K st len b1 > 0 holds
LineVec2Mx (((Mx2Tran (M,b1,b2)) . v1) |-- b2) = (LineVec2Mx (v1 |-- b1)) * M