theorem Th24: :: CATALG_1:24

for C1, C2 being Category
for F being Functor of C1,C2 holds Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2