let U be Universe; :: thesis: 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 U -small Category & nMatrixFieldCat (K,o,n) is U -locally_small Category )
let K be Field; :: thesis: 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 U -small Category & nMatrixFieldCat (K,o,n) is U -locally_small Category )
let o be Element of U; :: thesis: 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 U -small Category & nMatrixFieldCat (K,o,n) is U -locally_small Category )
let n be non zero Nat; :: thesis: ( the carrier of K is Element of U implies ( the carrier of (nMatrixFieldCat (K,o,n)) is trivial & nMatrixFieldCat (K,o,n) is U -small Category & nMatrixFieldCat (K,o,n) is U -locally_small Category ) )
assume A1: the carrier of K is Element of U ; :: thesis: ( the carrier of (nMatrixFieldCat (K,o,n)) is trivial & nMatrixFieldCat (K,o,n) is U -small Category & nMatrixFieldCat (K,o,n) is U -locally_small Category )
thus the carrier of (nMatrixFieldCat (K,o,n)) is trivial ; :: thesis: ( nMatrixFieldCat (K,o,n) is U -small Category & nMatrixFieldCat (K,o,n) is U -locally_small Category )

now :: thesis: ( the carrier of (nMatrixFieldCat (K,o,n)) in U & the carrier' of (nMatrixFieldCat (K,o,n)) in U )

A2: n -tuples_on the carrier of K in U by A1, CLASSES4:58;
thus the carrier of (nMatrixFieldCat (K,o,n)) in U by Th18; :: thesis: the carrier' of (nMatrixFieldCat (K,o,n)) in U
the carrier of (n -G_Matrix_over K) = n -Matrices_over K by MATRIX_1:def 7
.= n -tuples_on (n -tuples_on the carrier of K) by MATRIX_1:def 1 ;
hence the carrier' of (nMatrixFieldCat (K,o,n)) in U by A2, CLASSES4:58; :: thesis: verum

end;

then nMatrixFieldCat (K,o,n) is U -element ;
hence ( nMatrixFieldCat (K,o,n) is U -small Category & nMatrixFieldCat (K,o,n) is U -locally_small Category ) by Th96; :: thesis: verum