theorem Th72: :: CLASSES5:70
for U being Universe
for C, D being Category st C is U -element & D is U -element holds
Functors (C,D) is U -element