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
.= len (AutMt (g,b2,b3)) by Def8 ;
A5: width (AutMt ((g * f),b1,b3)) = len b3 by
.= width (AutMt (g,b2,b3)) by ;
then A6: width (AutMt ((g * f),b1,b3)) = width ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) by ;
A7: len (AutMt ((g * f),b1,b3)) = len b1 by Def8
.= len (AutMt (f,b1,b2)) by Def8
.= len ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) by ;
then A8: dom (AutMt ((g * f),b1,b3)) = dom ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) by FINSEQ_3:29;
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 H1( 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 = H1(k) ) ) from 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_0:def 4;
then A12: j in Seg (width (AutMt ((g * f),b1,b3))) by ZFMISC_1:87;
A13: len (Col ((AutMt (g,b2,b3)),j)) = len (AutMt (g,b2,b3)) by MATRIX_0:def 8
.= len d by ;
A14: dom d = Seg (len b2) by ;
A15: [i,j] in Indices ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) by ;
A16: i in dom (AutMt ((g * f),b1,b3)) by ;
A17: width (AutMt ((g * f),b1,b3)) <> {} by A12;
len b1 = len (AutMt ((g * f),b1,b3)) by Def8;
then len b1 > 0 by ;
then A18: j in Seg (len b3) by ;
then A19: j in dom b3 by FINSEQ_1:def 3;
A20: now :: thesis: for k being Nat st 1 <= k & k <= len d holds
(Col ((AutMt (g,b2,b3)),j)) . k = d . k
let k be Nat; :: thesis: ( 1 <= k & k <= len d implies (Col ((AutMt (g,b2,b3)),j)) . k = d . k )
assume A21: ( 1 <= k & k <= len d ) ; :: thesis: (Col ((AutMt (g,b2,b3)),j)) . k = d . k
then A22: k in dom d by FINSEQ_3:25;
A23: k in dom b2 by ;
A24: len (AutMt (g,b2,b3)) = len b2 by Def8;
then A25: k in dom (AutMt (g,b2,b3)) by ;
j in Seg (width (AutMt (g,b2,b3))) by ;
then [k,j] in [:(dom (AutMt (g,b2,b3))),(Seg (width (AutMt (g,b2,b3)))):] by ;
then [k,j] in Indices (AutMt (g,b2,b3)) by MATRIX_0:def 4;
then consider p2 being FinSequence of K such that
A26: p2 = (AutMt (g,b2,b3)) . k and
A27: (AutMt (g,b2,b3)) * (k,j) = p2 . j by MATRIX_0:def 5;
A28: p2 = (AutMt (g,b2,b3)) /. k by
.= (g . (b2 /. k)) |-- b3 by ;
then j in Seg (len p2) by ;
then A29: j in dom p2 by FINSEQ_1:def 3;
k in dom (AutMt (g,b2,b3)) by ;
hence (Col ((AutMt (g,b2,b3)),j)) . k = p2 . j by
.= ((g . (b2 /. k)) |-- b3) /. j by
.= d . k by ;
:: thesis: verum
end;
b1 /. i in the carrier of V1 ;
then A30: b1 /. i in dom f by FUNCT_2:def 1;
consider p1 being FinSequence of K such that
A31: p1 = (AutMt ((g * f),b1,b3)) . i and
A32: (AutMt ((g * f),b1,b3)) * (i,j) = p1 . j by ;
A33: len ((f . (b1 /. i)) |-- b2) = len b2 by Def7;
A34: len (AutMt ((g * f),b1,b3)) = len b1 by Def8;
then A35: i in dom b1 by ;
A36: p1 = (AutMt ((g * f),b1,b3)) /. i by
.= ((g * f) . (b1 /. i)) |-- b3 by ;
len (AutMt (f,b1,b2)) = len b1 by Def8;
then A37: i in dom (AutMt (f,b1,b2)) by ;
then A38: Line ((AutMt (f,b1,b2)),i) = (AutMt (f,b1,b2)) . i by MATRIX_0:60
.= (AutMt (f,b1,b2)) /. i by
.= (f . (b1 /. i)) |-- b2 by ;
A39: Seg (len b2) = dom b2 by FINSEQ_1:def 3;
j in Seg (len (((g * f) . (b1 /. i)) |-- b3)) by ;
then j in dom p1 by ;
hence (AutMt ((g * f),b1,b3)) * (i,j) = (((g * f) . (b1 /. i)) |-- b3) /. j by
.= ((g . (f . (b1 /. i))) |-- b3) /. j by
.= ((g . (Sum (lmlt (((f . (b1 /. i)) |-- b2),b2)))) |-- b3) /. j by Th35
.= ((Sum (lmlt (((f . (b1 /. i)) |-- b2),(g * b2)))) |-- b3) /. j by
.= Sum (mlt (((f . (b1 /. i)) |-- b2),d)) by A3, A19, A9, A14, A39, A33, Th37
.= (Line ((AutMt (f,b1,b2)),i)) "*" (Col ((AutMt (g,b2,b3)),j)) by
.= ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) * (i,j) by ;
:: thesis: verum
end;
hence AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) by ; :: thesis: verum