let o be Element of FinSETS ; :: thesis: for n being non zero Nat holds
( the carrier of (nMatrixFieldCat (F_Complex,o,n)) is trivial & the carrier of (nMatrixFieldCat (F_Complex,o,n)) is FinSETS -set & nMatrixFieldCat (F_Complex,o,n) is not FinSETS -small Category & nMatrixFieldCat (F_Complex,o,n) is not FinSETS -locally_small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -locally_small Category )
let n be non zero Nat; :: thesis: ( the carrier of (nMatrixFieldCat (F_Complex,o,n)) is trivial & the carrier of (nMatrixFieldCat (F_Complex,o,n)) is FinSETS -set & nMatrixFieldCat (F_Complex,o,n) is not FinSETS -small Category & nMatrixFieldCat (F_Complex,o,n) is not FinSETS -locally_small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -locally_small Category )
thus the carrier of (nMatrixFieldCat (F_Complex,o,n)) is trivial ; :: thesis: ( the carrier of (nMatrixFieldCat (F_Complex,o,n)) is FinSETS -set & nMatrixFieldCat (F_Complex,o,n) is not FinSETS -small Category & nMatrixFieldCat (F_Complex,o,n) is not FinSETS -locally_small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -locally_small Category )
thus the carrier of (nMatrixFieldCat (F_Complex,o,n)) is FinSETS -set by Th18; :: thesis: ( nMatrixFieldCat (F_Complex,o,n) is not FinSETS -small Category & nMatrixFieldCat (F_Complex,o,n) is not FinSETS -locally_small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -locally_small Category )

now :: thesis: nMatrixFieldCat (F_Complex,o,n) is not FinSETS -small Category

assume nMatrixFieldCat (F_Complex,o,n) is FinSETS -small Category ; :: thesis: contradiction
then A1: nMatrixFieldCat (F_Complex,o,n) is FinSETS -element ;
the carrier of (n -G_Matrix_over F_Complex) = n -Matrices_over F_Complex by MATRIX_1:def 7
.= n -tuples_on (n -tuples_on the carrier of F_Complex) by MATRIX_1:def 1 ;
then n -tuples_on the carrier of F_Complex is finite by A1, Th6;
hence contradiction by Th6; :: thesis: verum

end;

hence nMatrixFieldCat (F_Complex,o,n) is not FinSETS -small Category ; :: thesis: ( nMatrixFieldCat (F_Complex,o,n) is not FinSETS -locally_small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -locally_small Category )
reconsider x = o as Object of (nMatrixFieldCat (F_Complex,o,n)) by TARSKI:def 1;

A2: now :: thesis: ( Hom (x,x) c= the carrier' of (nMatrixFieldCat (F_Complex,o,n)) & the carrier' of (nMatrixFieldCat (F_Complex,o,n)) c= Hom (x,x) )

thus Hom (x,x) c= the carrier' of (nMatrixFieldCat (F_Complex,o,n)) ; :: thesis: the carrier' of (nMatrixFieldCat (F_Complex,o,n)) c= Hom (x,x)

now :: thesis: for oo being object st oo in the carrier' of (nMatrixFieldCat (F_Complex,o,n)) holds
oo in Hom (x,x)

let oo be object ; :: thesis: ( oo in the carrier' of (nMatrixFieldCat (F_Complex,o,n)) implies oo in Hom (x,x) )
assume oo in the carrier' of (nMatrixFieldCat (F_Complex,o,n)) ; :: thesis: oo in Hom (x,x)
then reconsider o9 = oo as Morphism of (nMatrixFieldCat (F_Complex,o,n)) ;
( dom o9 = o & cod o9 = o ) ;
hence oo in Hom (x,x) by CAT_1:1; :: thesis: verum

end;

hence the carrier' of (nMatrixFieldCat (F_Complex,o,n)) c= Hom (x,x) ; :: thesis: verum

end;

not Hom (x,x) is FinSETS -set

proof

assume A3: Hom (x,x) is FinSETS -set ; :: thesis: contradiction
the carrier of (n -G_Matrix_over F_Complex) = n -Matrices_over F_Complex by MATRIX_1:def 7
.= n -tuples_on (n -tuples_on the carrier of F_Complex) by MATRIX_1:def 1 ;
then n -tuples_on the carrier of F_Complex is finite by A3, A2, Th6;
hence contradiction by Th6; :: thesis: verum

end;

hence nMatrixFieldCat (F_Complex,o,n) is not FinSETS -locally_small Category by Def36; :: thesis: ( nMatrixFieldCat (F_Complex,o,n) is SETS -small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -locally_small Category )
A4: ( o in FinSETS & FinSETS c= SETS ) by CLASSES2:69;
( COMPLEX is Element of SETS & the carrier of F_Complex = COMPLEX ) by CLASSES4:21, CLASSES4:55, COMPLFLD:def 1;
hence ( nMatrixFieldCat (F_Complex,o,n) is SETS -small Category & nMatrixFieldCat (F_Complex,o,n) is SETS -locally_small Category ) by A4, Th111; :: thesis: verum