theorem :: CLASSES5:110

for o being Element of FinSETS
for n being non zero Nat holds
( the carrier of (nMatrixFieldCat (F_Real,o,n)) is trivial & the carrier of (nMatrixFieldCat (F_Real,o,n)) is FinSETS -set & nMatrixFieldCat (F_Real,o,n) is not FinSETS -small Category & nMatrixFieldCat (F_Real,o,n) is not FinSETS -locally_small Category & nMatrixFieldCat (F_Real,o,n) is SETS -small Category & nMatrixFieldCat (F_Real,o,n) is SETS -locally_small Category )