theorem Th65: :: CAT_8:65

for C1, C2 being non empty category
for f being morphism of (Functors (C1,C2)) ex F1, F2 being covariant Functor of C1,C2 ex T being natural_transformation of F1,F2 st
( f = [[F1,F2],T] & dom f = [[F1,F1],F1] & cod f = [[F2,F2],F2] )