let K be Field; :: thesis: for V1, V2, V3 being finite-dimensional VectSp of K
for f being Function of V1,V2
for g being Function of V2,V3
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for b3 being OrdBasis of V3 st f is linear & g is linear & len b1 > 0 & len b2 > 0 & len b3 > 0 holds
AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3)
let V1, V2, V3 be finite-dimensional VectSp of K; :: thesis: for f being Function of V1,V2
for g being Function of V2,V3
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for b3 being OrdBasis of V3 st f is linear & g is linear & len b1 > 0 & len b2 > 0 & len b3 > 0 holds
AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3)
let f be Function of V1,V2; :: thesis: for g being Function of V2,V3
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for b3 being OrdBasis of V3 st f is linear & g is linear & len b1 > 0 & len b2 > 0 & len b3 > 0 holds
AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3)
let g be Function of V2,V3; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for b3 being OrdBasis of V3 st f is linear & g is linear & len b1 > 0 & len b2 > 0 & len b3 > 0 holds
AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3)
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for b3 being OrdBasis of V3 st f is linear & g is linear & len b1 > 0 & len b2 > 0 & len b3 > 0 holds
AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3)
let b2 be OrdBasis of V2; :: thesis: for b3 being OrdBasis of V3 st f is linear & g is linear & len b1 > 0 & len b2 > 0 & len b3 > 0 holds
AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3)
let b3 be OrdBasis of V3; :: thesis: ( f is linear & g is linear & len b1 > 0 & len b2 > 0 & len b3 > 0 implies AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3) )
assume A1: ( f is linear & g is linear ) ; :: thesis: ( not len b1 > 0 or not len b2 > 0 or not len b3 > 0 or AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3) )
assume A2: ( len b1 > 0 & len b2 > 0 & len b3 > 0 ) ; :: thesis: AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3)
then A3: width (AutMt f,b1,b2) = len b2 by Th44
.= len (AutMt g,b2,b3) by Def10 ;
A4: len (AutMt (g * f),b1,b3) = len b1 by Def10
.= len (AutMt f,b1,b2) by Def10
.= len ((AutMt f,b1,b2) * (AutMt g,b2,b3)) by A3, MATRIX_3:def 4 ;
then A5: dom (AutMt (g * f),b1,b3) = dom ((AutMt f,b1,b2) * (AutMt g,b2,b3)) by FINSEQ_3:31;
A6: width (AutMt (g * f),b1,b3) = len b3 by A2, Th44
.= width (AutMt g,b2,b3) by A2, Th44 ;
then A7: width (AutMt (g * f),b1,b3) = width ((AutMt f,b1,b2) * (AutMt g,b2,b3)) by A3, MATRIX_3:def 4;
for i, j being Nat st [i,j] in Indices (AutMt (g * f),b1,b3) holds
(AutMt (g * f),b1,b3) * i,j = ((AutMt f,b1,b2) * (AutMt g,b2,b3)) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (AutMt (g * f),b1,b3) implies (AutMt (g * f),b1,b3) * i,j = ((AutMt f,b1,b2) * (AutMt g,b2,b3)) * i,j )
assume A8: [i,j] in Indices (AutMt (g * f),b1,b3) ; :: thesis: (AutMt (g * f),b1,b3) * i,j = ((AutMt f,b1,b2) * (AutMt g,b2,b3)) * i,j
then A9: [i,j] in [:(dom (AutMt (g * f),b1,b3)),(Seg (width (AutMt (g * f),b1,b3))):] by MATRIX_1:def 5;
then A10: [i,j] in Indices ((AutMt f,b1,b2) * (AutMt g,b2,b3)) by A5, A7, MATRIX_1:def 5;
A11: i in dom (AutMt (g * f),b1,b3) by A9, ZFMISC_1:106;
A12: len (AutMt (g * f),b1,b3) = len b1 by Def10;
then A13: i in dom b1 by A11, FINSEQ_3:31;
consider p1 being FinSequence of K such that
A14: ( p1 = (AutMt (g * f),b1,b3) . i & (AutMt (g * f),b1,b3) * i,j = p1 . j ) by A8, MATRIX_1:def 6;
A15: j in Seg (width (AutMt (g * f),b1,b3)) by A9, ZFMISC_1:106;
len b1 = len (AutMt (g * f),b1,b3) by Def10;
then len b1 > 0 by A15, FINSEQ_1:4, MATRIX_1:def 4;
then A16: j in Seg (len b3) by A15, Th44;
then A17: j in dom b3 by FINSEQ_1:def 3;
A18: p1 = (AutMt (g * f),b1,b3) /. i by A11, A14, PARTFUN1:def 8
.= ((g * f) . (b1 /. i)) |-- b3 by A13, Def10 ;
j in Seg (len (((g * f) . (b1 /. i)) |-- b3)) by A16, Def9;
then A19: j in dom p1 by A18, FINSEQ_1:def 3;
deffunc H₁( Nat) -> Element of the carrier of K = ((g . (b2 /. $1)) |-- b3) /. j;
consider d being FinSequence of K such that
A20: ( len d = len b2 & ( for k being Nat st k in dom d holds
d . k = H₁(k) ) ) from FINSEQ_2:sch 1();
A21: dom d = Seg (len b2) by A20, FINSEQ_1:def 3;
A22: Seg (len b2) = dom b2 by FINSEQ_1:def 3;
len (AutMt f,b1,b2) = len b1 by Def10;
then A23: i in dom (AutMt f,b1,b2) by A11, A12, FINSEQ_3:31;
then A24: Line (AutMt f,b1,b2),i = (AutMt f,b1,b2) . i by MATRIX_2:18
.= (AutMt f,b1,b2) /. i by A23, PARTFUN1:def 8
.= (f . (b1 /. i)) |-- b2 by A13, Def10 ;
A25: len (Col (AutMt g,b2,b3),j) = len (AutMt g,b2,b3) by MATRIX_1:def 9
.= len d by A20, Def10 ;

A26: now

let k be Nat; :: thesis: ( 1 <= k & k <= len d implies (Col (AutMt g,b2,b3),j) . k = d . k )
assume A27: ( 1 <= k & k <= len d ) ; :: thesis: (Col (AutMt g,b2,b3),j) . k = d . k
then A28: k in dom d by FINSEQ_3:27;
A30: len (AutMt g,b2,b3) = len b2 by Def10;
then A31: ( k in dom (AutMt g,b2,b3) & j in Seg (width (AutMt g,b2,b3)) ) by A6, A9, A20, A27, FINSEQ_3:27, ZFMISC_1:106;
then [k,j] in [:(dom (AutMt g,b2,b3)),(Seg (width (AutMt g,b2,b3))):] by ZFMISC_1:106;
then [k,j] in Indices (AutMt g,b2,b3) by MATRIX_1:def 5;
then consider p2 being FinSequence of K such that
A32: ( p2 = (AutMt g,b2,b3) . k & (AutMt g,b2,b3) * k,j = p2 . j ) by MATRIX_1:def 6;
A33: k in dom (AutMt g,b2,b3) by A20, A27, A30, FINSEQ_3:27;
A34: k in dom b2 by A20, A27, FINSEQ_3:27;
A35: p2 = (AutMt g,b2,b3) /. k by A31, A32, PARTFUN1:def 8
.= (g . (b2 /. k)) |-- b3 by A34, Def10 ;
then j in Seg (len p2) by A16, Def9;
then A36: j in dom p2 by FINSEQ_1:def 3;
thus (Col (AutMt g,b2,b3),j) . k = p2 . j by A32, A33, MATRIX_1:def 9
.= ((g . (b2 /. k)) |-- b3) /. j by A35, A36, PARTFUN1:def 8
.= d . k by A20, A28 ; :: thesis: verum

end;

b1 /. i in the carrier of V1 ;
then A37: b1 /. i in dom f by FUNCT_2:def 1;
A38: len ((f . (b1 /. i)) |-- b2) = len b2 by Def9;
thus (AutMt (g * f),b1,b3) * i,j = (((g * f) . (b1 /. i)) |-- b3) /. j by A14, A18, A19, PARTFUN1:def 8
.= ((g . (f . (b1 /. i))) |-- b3) /. j by A37, FUNCT_1:23
.= ((g . (Sum (lmlt ((f . (b1 /. i)) |-- b2),b2))) |-- b3) /. j by Th40
.= ((Sum (lmlt ((f . (b1 /. i)) |-- b2),(g * b2))) |-- b3) /. j by A1, A38, Th22
.= Sum (mlt ((f . (b1 /. i)) |-- b2),d) by A2, A17, A20, A22, A38, Th42, A21
.= (Line (AutMt f,b1,b2),i) "*" (Col (AutMt g,b2,b3),j) by A24, A25, A26, FINSEQ_1:18
.= ((AutMt f,b1,b2) * (AutMt g,b2,b3)) * i,j by A3, A10, MATRIX_3:def 4 ; :: thesis: verum

end;

hence AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3) by A4, A7, MATRIX_1:21; :: thesis: verum