set C = nMatrixFieldCat (K,o,n);
reconsider M = 0. (K,n) as Element of n -Matrices_over K by MATRIX_1:2;
the carrier of (n -G_Matrix_over K) = n -Matrices_over K by MATRIX_1:def 7;
then M in the carrier of (n -G_Matrix_over K) ;
then reconsider M = 0. (K,n) as Element of the carrier of (n -G_Matrix_over K) ;
reconsider M9 = M as Morphism of (nMatrixFieldCat (K,o,n)) ;
A1: ( dom M9 = o & cod M9 = o ) ;
set cC = the carrier of (n -G_Matrix_over K);

A2: now :: thesis: 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)); :: thesis: ( [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; :: thesis: verum

end;

now :: thesis: for a being Element of (nMatrixFieldCat (K,o,n)) ex i being Morphism of a,a st
for b being Element of (nMatrixFieldCat (K,o,n)) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )

let a be Element of (nMatrixFieldCat (K,o,n)); :: thesis: ex i being Morphism of a,a st
for b being Element of (nMatrixFieldCat (K,o,n)) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
a = o by TARSKI:def 1;
then M9 in Hom (a,a) by CAT_1:1, A1;
then reconsider i = M9 as Morphism of a,a by CAT_1:def 5;

now :: thesis: for b being Element of (nMatrixFieldCat (K,o,n)) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )

let b be Element of (nMatrixFieldCat (K,o,n)); :: thesis: ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )

hereby :: thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )

assume Hom (a,b) <> {} ; :: thesis: for g being Morphism of a,b holds g (*) i = g

hereby :: thesis: verum

let g be Morphism of a,b; :: thesis: g (*) i = g
reconsider g9 = g, i9 = i as Element of n -Matrices_over K by MATRIX_1:def 7;
reconsider g99 = g9, i99 = i9 as Matrix of n,K by MATRIX_1:2;
A3: the Comp of (nMatrixFieldCat (K,o,n)) . (g,i) = g99 + i99 by MATRIX_1:def 7;
reconsider gi9 = g (*) i as Element of n -Matrices_over K by MATRIX_1:def 7;
dom g = cod i ;
then g (*) i = g99 + i99 by A2, CAT_1:def 1, A3
.= g99 by MATRIX_1:5 ;
hence g (*) i = g ; :: thesis: verum

end;

end;

hereby :: thesis: verum

assume Hom (b,a) <> {} ; :: thesis: for f being Morphism of b,a holds i (*) f = f

hereby :: thesis: verum

let f be Morphism of b,a; :: thesis: i (*) f = f
reconsider f9 = f, i9 = i as Element of n -Matrices_over K by MATRIX_1:def 7;
reconsider f99 = f9, i99 = i9 as Matrix of n,K by MATRIX_1:2;
A4: the Comp of (nMatrixFieldCat (K,o,n)) . (i,f) = i99 + f99 by MATRIX_1:def 7;
reconsider if9 = i (*) f as Element of n -Matrices_over K by MATRIX_1:def 7;
dom i = cod f ;
then i (*) f = i99 + f99 by A2, CAT_1:def 1, A4
.= f99 + i99 by MATRIX_1:3
.= f99 by MATRIX_1:5 ;
hence i (*) f = f ; :: thesis: verum

end;

end;

end;

hence ex i being Morphism of a,a st
for b being Element of (nMatrixFieldCat (K,o,n)) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) ; :: thesis: verum

end;

hence nMatrixFieldCat (K,o,n) is with_identities by CAT_1:def 10; :: thesis: verum