let U be Universe; :: thesis: for C, D being U -small Category holds
( Functors (C,D) is U -small & NatTrans (C,D) is U -set )
let C, D be U -small Category; :: thesis: ( Functors (C,D) is U -small & NatTrans (C,D) is U -set )
thus Functors (C,D) is U -small by Th72; :: thesis: NatTrans (C,D) is U -set
then the carrier' of (Functors (C,D)) in U ;
hence NatTrans (C,D) is U -set by NATTRA_1:def 17; :: thesis: verum