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, Th39
.= len (AutMt (g,b2,b3)) by Def8 ;
A5: width (AutMt ((g * f),b1,b3)) = len b3 by A2, Th39
.= width (AutMt (g,b2,b3)) by A3, Th39 ;
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 Def8
.= len (AutMt (f,b1,b2)) by Def8
.= 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: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 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_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 A9, Def8 ;
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_0:def 4;
A16: i in dom (AutMt ((g * f),b1,b3)) by A11, ZFMISC_1:87;
A17: width (AutMt ((g * f),b1,b3)) <> {} by A12;
len b1 = len (AutMt ((g * f),b1,b3)) by Def8;
then len b1 > 0 by A17, MATRIX_0:def 3;
then A18: j in Seg (len b3) by A12, Th39;
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 A9, A21, FINSEQ_3:25;
A24: len (AutMt (g,b2,b3)) = len b2 by Def8;
then A25: k in dom (AutMt (g,b2,b3)) by A9, A21, FINSEQ_3:25;
j in Seg (width (AutMt (g,b2,b3))) by A5, A11, ZFMISC_1:87;
then [k,j] in [:(dom (AutMt (g,b2,b3))),(Seg (width (AutMt (g,b2,b3)))):] by A25, ZFMISC_1:87;
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 A25, A26, PARTFUN1:def 6
.= (g . (b2 /. k)) |-- b3 by A23, Def8 ;
then j in Seg (len p2) by A18, Def7;
then A29: j in dom p2 by FINSEQ_1:def 3;
k in dom (AutMt (g,b2,b3)) by A9, A21, A24, FINSEQ_3:25;
hence (Col ((AutMt (g,b2,b3)),j)) . k = p2 . j by A27, MATRIX_0:def 8
.= ((g . (b2 /. k)) |-- b3) /. j by A28, A29, PARTFUN1:def 6
.= d . k by A9, A22 ;
:: 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 A10, MATRIX_0:def 5;
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 A16, FINSEQ_3:29;
A36: p1 = (AutMt ((g * f),b1,b3)) /. i by A16, A31, PARTFUN1:def 6
.= ((g * f) . (b1 /. i)) |-- b3 by A35, Def8 ;
len (AutMt (f,b1,b2)) = len b1 by Def8;
then A37: i in dom (AutMt (f,b1,b2)) by A16, A34, FINSEQ_3:29;
then A38: Line ((AutMt (f,b1,b2)),i) = (AutMt (f,b1,b2)) . i by MATRIX_0:60
.= (AutMt (f,b1,b2)) /. i by A37, PARTFUN1:def 6
.= (f . (b1 /. i)) |-- b2 by A35, Def8 ;
A39: Seg (len b2) = dom b2 by FINSEQ_1:def 3;
j in Seg (len (((g * f) . (b1 /. i)) |-- b3)) by A18, Def7;
then j in dom p1 by A36, FINSEQ_1:def 3;
hence (AutMt ((g * f),b1,b3)) * (i,j) = (((g * f) . (b1 /. i)) |-- b3) /. j by A32, A36, PARTFUN1:def 6
.= ((g . (f . (b1 /. i))) |-- b3) /. j by A30, FUNCT_1:13
.= ((g . (Sum (lmlt (((f . (b1 /. i)) |-- b2),b2)))) |-- b3) /. j by Th35
.= ((Sum (lmlt (((f . (b1 /. i)) |-- b2),(g * b2)))) |-- b3) /. j by A1, A33, Th18
.= 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 A38, A13, A20, FINSEQ_1:14
.= ((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_0:21; :: thesis: verum