theorem Th64: :: CAT_8:64
for C1, C2 being non empty category
for f being morphism of (Functors (C1,C2)) holds
( f is identity iff ex F being covariant Functor of C1,C2 st f = [[F,F],F] )