theorem Th111: :: CLASSES5:109

for U being Universe
for K being Field
for o being Element of U
for n being non zero Nat st the carrier of K is Element of U holds
( the carrier of (nMatrixFieldCat (K,o,n)) is trivial & nMatrixFieldCat (K,o,n) is b₁ -small Category & nMatrixFieldCat (K,o,n) is b₁ -locally_small Category )