set C = nMatrixFieldCat (K,o,n);
now for f, g, h being Morphism of (nMatrixFieldCat (K,o,n)) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) flet f,
g,
h be
Morphism of
(nMatrixFieldCat (K,o,n));
( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )assume that
dom h = cod g
and
dom g = cod f
;
h (*) (g (*) f) = (h (*) g) (*) fset cC = the
carrier of
(n -G_Matrix_over K);
A1:
now for f, g being Morphism of (nMatrixFieldCat (K,o,n)) holds
( [g,f] in dom the Comp of (nMatrixFieldCat (K,o,n)) iff dom g = cod f )let f,
g be
Morphism of
(nMatrixFieldCat (K,o,n));
( [g,f] in dom the Comp of (nMatrixFieldCat (K,o,n)) iff dom g = cod f )
(
[g,f] in dom the
Comp of
(nMatrixFieldCat (K,o,n)) iff
[g,f] in [: the carrier of (n -G_Matrix_over K), the carrier of (n -G_Matrix_over K):] )
by PARTFUN1:def 2;
hence
(
[g,f] in dom the
Comp of
(nMatrixFieldCat (K,o,n)) iff
dom g = cod f )
by ZFMISC_1:87;
verum end; reconsider f9 =
f,
g9 =
g,
h9 =
h as
Element of
n -Matrices_over K by MATRIX_1:def 7;
reconsider f99 =
f9,
g99 =
g9,
h99 =
h9 as
Matrix of
n,
K by MATRIX_1:2;
set cC = the
carrier of
(n -G_Matrix_over K);
A2:
the
Comp of
(nMatrixFieldCat (K,o,n)) . (
g,
f)
= g99 + f99
by MATRIX_1:def 7;
A3:
the
Comp of
(nMatrixFieldCat (K,o,n)) . (
h,
g)
= h99 + g99
by MATRIX_1:def 7;
reconsider gf9 =
g (*) f,
hg9 =
h (*) g as
Element of
n -Matrices_over K by MATRIX_1:def 7;
reconsider gf99 =
gf9,
hg99 =
hg9 as
Matrix of
n,
K by MATRIX_1:2;
A4:
dom g = cod f
;
A5:
gf99 = g99 + f99
by A4, A1, CAT_1:def 1, A2;
dom h = cod g
;
then A6:
hg99 = h99 + g99
by A1, CAT_1:def 1, A3;
A7: the
addF of
(n -G_Matrix_over K) . (
h9,
gf9) =
h99 + (g99 + f99)
by A5, MATRIX_1:def 7
.=
(h99 + g99) + f99
by MATRIX_1:4
.=
the
addF of
(n -G_Matrix_over K) . (
hg9,
f9)
by A6, MATRIX_1:def 7
;
A8:
(
dom h = cod (g (*) f) &
dom (h (*) g) = cod f )
;
thus h (*) (g (*) f) =
the
addF of
(n -G_Matrix_over K) . (
h9,
gf9)
by A8, A1, CAT_1:def 1
.=
(h (*) g) (*) f
by A7, A1, A8, CAT_1:def 1
;
verum end;
hence
nMatrixFieldCat (K,o,n) is associative
by CAT_1:def 8; verum