let U be Universe; :: thesis: for C, D being CategorySet st C is U -set & D is U -set holds
Functors (C,D) is U -set
let C, D be CategorySet; :: thesis: ( C is U -set & D is U -set implies Functors (C,D) is U -set )
assume that
A1: C is U -set and
A2: D is U -set ; :: thesis: Functors (C,D) is U -set
( SetToCat C is U -element & SetToCat D is U -element ) by A1, A2, Th89;
then Functors ((SetToCat C),(SetToCat D)) is U -element by Th72;
hence Functors (C,D) is U -set by Th88; :: thesis: verum