theorem
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))