for K being Field
for V1, V2, V3 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for B3 being FinSequence of V3
for A being Matrix of len b1, len b2,K
for B being Matrix of len b2, len B3,K st width A = len B holds
for AB being Matrix of len b1, len B3,K st AB = A * B holds
Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))