let K be Field; :: thesis: 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))
let V1, V2, V3 be finite-dimensional VectSp of K; :: thesis: 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))
let b1 be OrdBasis of V1; :: thesis: 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))
let b2 be OrdBasis of V2; :: thesis: 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))
let B3 be FinSequence of V3; :: thesis: 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))
let A be Matrix of len b1, len b2,K; :: thesis: 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))
let B be Matrix of len b2, len B3,K; :: thesis: ( width A = len B implies 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)) )
assume A1: width A = len B ; :: thesis: 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))
set MB = Mx2Tran (B,b2,B3);
set MA = Mx2Tran (A,b1,b2);
let AB be Matrix of len b1, len B3,K; :: thesis: ( AB = A * B implies Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2)) )
assume A2: AB = A * B ; :: thesis: Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))
set MAB = Mx2Tran (AB,b1,B3);

now :: thesis: for x being object st x in the carrier of V1 holds
((Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))) . x = (Mx2Tran (AB,b1,B3)) . x

let x be object ; :: thesis: ( x in the carrier of V1 implies ((Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))) . x = (Mx2Tran (AB,b1,B3)) . x )
assume x in the carrier of V1 ; :: thesis: ((Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))) . x = (Mx2Tran (AB,b1,B3)) . x
then reconsider v = x as Element of V1 ;
set L = LineVec2Mx (v |-- b1);
A3: len A = len b1 by MATRIX_0:def 2;
A4: ( width (LineVec2Mx (v |-- b1)) = len (v |-- b1) & len (v |-- b1) = len b1 ) by MATRIX_0:23, MATRLIN:def 7;
then ( len (LineVec2Mx (v |-- b1)) = 1 & len ((LineVec2Mx (v |-- b1)) * A) = len (LineVec2Mx (v |-- b1)) ) by A3, MATRIX_0:23, MATRIX_3:def 4;
then A5: dom ((LineVec2Mx (v |-- b1)) * A) = Seg 1 by FINSEQ_1:def 3;
A6: width ((LineVec2Mx (v |-- b1)) * A) = width A by A4, A3, MATRIX_3:def 4;
then A7: ( len B = len b2 & len (Line (((LineVec2Mx (v |-- b1)) * A),1)) = width A ) by CARD_1:def 7, MATRIX_0:def 2;
A8: 1 in Seg 1 ;
dom ((Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))) = the carrier of V1 by FUNCT_2:def 1;
hence ((Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))) . x = (Mx2Tran (B,b2,B3)) . ((Mx2Tran (A,b1,b2)) . v) by FUNCT_1:12
.= (Mx2Tran (B,b2,B3)) . (Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),b2))) by Def3
.= Sum (lmlt ((Line (((LineVec2Mx ((Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),b2))) |-- b2)) * B),1)),B3)) by Def3
.= Sum (lmlt ((Line (((LineVec2Mx (Line (((LineVec2Mx (v |-- b1)) * A),1))) * B),1)),B3)) by A1, A7, MATRLIN:36
.= Sum (lmlt ((Line ((LineVec2Mx (Line ((((LineVec2Mx (v |-- b1)) * A) * B),1))),1)),B3)) by A1, A6, A5, A8, Th35
.= Sum (lmlt ((Line ((LineVec2Mx (Line (((LineVec2Mx (v |-- b1)) * AB),1))),1)),B3)) by A1, A2, A4, A3, MATRIX_3:33
.= Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * AB),1)),B3)) by MATRIX15:25
.= (Mx2Tran (AB,b1,B3)) . x by Def3 ;
:: thesis: verum

end;

hence Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2)) by FUNCT_2:12; :: thesis: verum