:: deftheorem defines nMatrixFieldCat CLASSES5:def 37 :
for K being Field
for o being object
for n being Nat holds nMatrixFieldCat (K,o,n) = CatStr(# {o}, the carrier of (n -G_Matrix_over K),( the carrier of (n -G_Matrix_over K) --> o),( the carrier of (n -G_Matrix_over K) --> o),(# (n -G_Matrix_over K)) #);