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)
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;
set MA = Mx2Tran A,b1,b2;
set MB = Mx2Tran B,b2,B3;

now

let x be set ; :: thesis: ( x in the carrier of V1 implies ((Mx2Tran B,b2,B3) * (Mx2Tran A,b1,b2)) . x = (Mx2Tran AB,b1,B3) . x )
assume A3: x in the carrier of V1 ; :: thesis: ((Mx2Tran B,b2,B3) * (Mx2Tran A,b1,b2)) . x = (Mx2Tran AB,b1,B3) . x
reconsider v = x as Element of V1 by A3;
set L = LineVec2Mx (v |-- b1);
A4: ( len (LineVec2Mx (v |-- b1)) = 1 & width (LineVec2Mx (v |-- b1)) = len (v |-- b1) & len (v |-- b1) = len b1 & len A = len b1 & len B = len b2 ) by MATRIX_1:24, MATRIX_1:def 3, MATRLIN:def 9;
then A5: ( len ((LineVec2Mx (v |-- b1)) * A) = len (LineVec2Mx (v |-- b1)) & width ((LineVec2Mx (v |-- b1)) * A) = width A ) by MATRIX_3:def 4;
then A6: ( dom ((LineVec2Mx (v |-- b1)) * A) = Seg 1 & 1 in Seg 1 & len (Line ((LineVec2Mx (v |-- b1)) * A),1) = width A ) by A4, FINSEQ_1:def 3, FINSEQ_1:def 18;
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:22
.= (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, A4, A6, MATRLIN:41
.= Sum (lmlt (Line (LineVec2Mx (Line (((LineVec2Mx (v |-- b1)) * A) * B),1)),1),B3) by A1, A5, A6, Th35
.= Sum (lmlt (Line (LineVec2Mx (Line ((LineVec2Mx (v |-- b1)) * AB),1)),1),B3) by A1, A2, A4, MATRIX_3:35
.= 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:18; :: thesis: verum