set C = nMatrixFieldCat (K,o,n);

now :: thesis: for b being Element of (nMatrixFieldCat (K,o,n)) holds Hom (b,b) <> {}

let b be Element of (nMatrixFieldCat (K,o,n)); :: thesis: Hom (b,b) <> {}
A1: b = o by TARSKI:def 1;
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)) ;
( dom M9 = o & cod M9 = o ) ;
hence Hom (b,b) <> {} by A1, CAT_1:1; :: thesis: verum

end;

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