set cC = the carrier of (n -G_Matrix_over K);
set C = nMatrixFieldCat (K,o,n);

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;

hence nMatrixFieldCat (K,o,n) is Category-like by CAT_1:def 6; :: thesis: verum