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 g is additive & g is homogeneous & len b1 > 0 & len b2 > 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 g is additive & g is homogeneous & len b1 > 0 & len b2 > 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 g is additive & g is homogeneous & len b1 > 0 & len b2 > 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 g is additive & g is homogeneous & len b1 > 0 & len b2 > 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 g is additive & g is homogeneous & len b1 > 0 & len b2 > 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 g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds
AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3)
let b3 be OrdBasis of V3; :: thesis: ( g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 implies AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3) )
assume A1: ( g is additive & g is homogeneous ) ; :: thesis: ( not len b1 > 0 or not len b2 > 0 or AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3) )
assume that
A2: len b1 > 0 and
A3: len b2 > 0 ; :: thesis: AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3)
A4: width (AutMt f,b1,b2) = len b2 by A2, Th44
.= len (AutMt g,b2,b3) by Def10 ;
A5: width (AutMt (g * f),b1,b3) = len b3 by A2, Th44
.= width (AutMt g,b2,b3) by A3, Th44 ;
then A6: width (AutMt (g * f),b1,b3) = width ((AutMt f,b1,b2) * (AutMt g,b2,b3)) by A4, MATRIX_3:def 4;
A7: 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 A4, MATRIX_3:def 4 ;
then A8: dom (AutMt (g * f),b1,b3) = dom ((AutMt f,b1,b2) * (AutMt g,b2,b3)) by FINSEQ_3:31;
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 )
deffunc H₁( Nat) -> Element of the carrier of K = ((g . (b2 /. $1)) |-- b3) /. j;
consider d being FinSequence of K such that
A9: ( len d = len b2 & ( for k being Nat st k in dom d holds
d . k = H₁(k) ) ) from FINSEQ_2:sch 1();
assume A10: [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 A11: [i,j] in [:(dom (AutMt (g * f),b1,b3)),(Seg (width (AutMt (g * f),b1,b3))):] by MATRIX_1:def 5;
then A12: j in Seg (width (AutMt (g * f),b1,b3)) by ZFMISC_1:106;
A13: len (Col (AutMt g,b2,b3),j) = len (AutMt g,b2,b3) by MATRIX_1:def 9
.= len d by A9, Def10 ;
A14: dom d = Seg (len b2) by A9, FINSEQ_1:def 3;
A15: [i,j] in Indices ((AutMt f,b1,b2) * (AutMt g,b2,b3)) by A8, A6, A11, MATRIX_1:def 5;
A16: i in dom (AutMt (g * f),b1,b3) by A11, ZFMISC_1:106;
X: width (AutMt (g * f),b1,b3) <> {} by A12;
len b1 = len (AutMt (g * f),b1,b3) by Def10;
then len b1 > 0 by X, MATRIX_1:def 4;
then A17: j in Seg (len b3) by A12, Th44;
then A18: j in dom b3 by FINSEQ_1:def 3;

A19: now

let k be Nat; :: thesis: ( 1 <= k & k <= len d implies (Col (AutMt g,b2,b3),j) . k = d . k )
assume A20: ( 1 <= k & k <= len d ) ; :: thesis: (Col (AutMt g,b2,b3),j) . k = d . k
then A21: k in dom d by FINSEQ_3:27;
A22: k in dom b2 by A9, A20, FINSEQ_3:27;
A23: len (AutMt g,b2,b3) = len b2 by Def10;
then A24: k in dom (AutMt g,b2,b3) by A9, A20, FINSEQ_3:27;
j in Seg (width (AutMt g,b2,b3)) by A5, A11, ZFMISC_1:106;
then [k,j] in [:(dom (AutMt g,b2,b3)),(Seg (width (AutMt g,b2,b3))):] by A24, 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
A25: p2 = (AutMt g,b2,b3) . k and
A26: (AutMt g,b2,b3) * k,j = p2 . j by MATRIX_1:def 6;
A27: p2 = (AutMt g,b2,b3) /. k by A24, A25, PARTFUN1:def 8
.= (g . (b2 /. k)) |-- b3 by A22, Def10 ;
then j in Seg (len p2) by A17, Def9;
then A28: j in dom p2 by FINSEQ_1:def 3;
k in dom (AutMt g,b2,b3) by A9, A20, A23, FINSEQ_3:27;
hence (Col (AutMt g,b2,b3),j) . k = p2 . j by A26, MATRIX_1:def 9
.= ((g . (b2 /. k)) |-- b3) /. j by A27, A28, PARTFUN1:def 8
.= d . k by A9, A21 ;
:: thesis: verum

end;

b1 /. i in the carrier of V1 ;
then A29: b1 /. i in dom f by FUNCT_2:def 1;
consider p1 being FinSequence of K such that
A30: p1 = (AutMt (g * f),b1,b3) . i and
A31: (AutMt (g * f),b1,b3) * i,j = p1 . j by A10, MATRIX_1:def 6;
A32: len ((f . (b1 /. i)) |-- b2) = len b2 by Def9;
A33: len (AutMt (g * f),b1,b3) = len b1 by Def10;
then A34: i in dom b1 by A16, FINSEQ_3:31;
A35: p1 = (AutMt (g * f),b1,b3) /. i by A16, A30, PARTFUN1:def 8
.= ((g * f) . (b1 /. i)) |-- b3 by A34, Def10 ;
len (AutMt f,b1,b2) = len b1 by Def10;
then A36: i in dom (AutMt f,b1,b2) by A16, A33, FINSEQ_3:31;
then A37: Line (AutMt f,b1,b2),i = (AutMt f,b1,b2) . i by MATRIX_2:18
.= (AutMt f,b1,b2) /. i by A36, PARTFUN1:def 8
.= (f . (b1 /. i)) |-- b2 by A34, Def10 ;
A38: Seg (len b2) = dom b2 by FINSEQ_1:def 3;
j in Seg (len (((g * f) . (b1 /. i)) |-- b3)) by A17, Def9;
then j in dom p1 by A35, FINSEQ_1:def 3;
hence (AutMt (g * f),b1,b3) * i,j = (((g * f) . (b1 /. i)) |-- b3) /. j by A31, A35, PARTFUN1:def 8
.= ((g . (f . (b1 /. i))) |-- b3) /. j by A29, 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, A32, Th22
.= Sum (mlt ((f . (b1 /. i)) |-- b2),d) by A3, A18, A9, A14, A38, A32, Th42
.= (Line (AutMt f,b1,b2),i) "*" (Col (AutMt g,b2,b3),j) by A37, A13, A19, FINSEQ_1:18
.= ((AutMt f,b1,b2) * (AutMt g,b2,b3)) * i,j by A4, A15, MATRIX_3:def 4 ;
:: thesis: verum

end;

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