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)

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

hence
AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))
by A7, A6, MATRIX_0:21; :: thesis: verum
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_{1}( 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_{1}(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;

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;deffunc H

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

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

b1 /. i in the carrier of V1
;(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;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

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