let U be Universe; :: thesis: for C, D being Category st C is U -element & D is U -element holds
Functors (C,D) is U -element
let C, D be Category; :: thesis: ( C is U -element & D is U -element implies Functors (C,D) is U -element )
assume that
A1: C is U -element and
A2: D is U -element ; :: thesis: Functors (C,D) is U -element
set E = Functors (C,D);
reconsider cC = the carrier of C, c9C = the carrier' of C, cD = the carrier of D, c9D = the carrier' of D as Element of U by A1, A2;

now :: thesis: ( the carrier of (Functors (C,D)) is Element of U & the carrier' of (Functors (C,D)) is Element of U & the Source of (Functors (C,D)) is Element of U & the Target of (Functors (C,D)) is Element of U & the Comp of (Functors (C,D)) is Element of U )

the carrier of (Functors (C,D)) = Funct (C,D) by NATTRA_1:def 17;
then A3: the carrier of (Functors (C,D)) c= bool [:c9C,c9D:] by Th68;
hence the carrier of (Functors (C,D)) is Element of U by CLASSES4:13; :: thesis: ( the carrier' of (Functors (C,D)) is Element of U & the Source of (Functors (C,D)) is Element of U & the Target of (Functors (C,D)) is Element of U & the Comp of (Functors (C,D)) is Element of U )
reconsider cE = the carrier of (Functors (C,D)) as Element of U by A3, CLASSES4:13;
the carrier' of (Functors (C,D)) = NatTrans (C,D) by NATTRA_1:def 17;
then A4: the carrier' of (Functors (C,D)) c= [:[:(bool [:c9C,c9D:]),(bool [:c9C,c9D:]):],(bool [:cC,c9D:]):] by Th69;
hence the carrier' of (Functors (C,D)) is Element of U by CLASSES4:13; :: thesis: ( the Source of (Functors (C,D)) is Element of U & the Target of (Functors (C,D)) is Element of U & the Comp of (Functors (C,D)) is Element of U )
reconsider c9E = the carrier' of (Functors (C,D)) as Element of U by A4, CLASSES4:13;
A5: the Source of (Functors (C,D)) in Funcs (c9E,cE) by FUNCT_2:8;
A6: ( Funcs (c9E,cE) is Element of U & U is axiom_GU1 & U is axiom_GU3 ) ;
hence the Source of (Functors (C,D)) is Element of U by A5; :: thesis: ( the Target of (Functors (C,D)) is Element of U & the Comp of (Functors (C,D)) is Element of U )
the Target of (Functors (C,D)) in Funcs (c9E,cE) by FUNCT_2:8;
hence the Target of (Functors (C,D)) is Element of U by A6; :: thesis: the Comp of (Functors (C,D)) is Element of U
the Comp of (Functors (C,D)) c= [:[:c9E,c9E:],c9E:] ;
hence the Comp of (Functors (C,D)) is Element of U by CLASSES4:13; :: thesis: verum

end;

hence Functors (C,D) is U -element ; :: thesis: verum