theorem Th63: :: CAT_8:63

for C1, C2 being non empty category
for f1, f2 being morphism of (Functors (C1,C2)) holds
( f1 |> f2 iff ex F, F1, F2 being covariant Functor of C1,C2 ex T1 being natural_transformation of F1,F ex T2 being natural_transformation of F,F2 st
( f1 = [[F,F2],T2] & f2 = [[F1,F],T1] & f1 (*) f2 = [[F1,F2],(T2 `*` T1)] & ( for g1, g2 being morphism of C1 st g2 |> g1 holds
( T2 . g2 |> T1 . g1 & (T2 `*` T1) . (g2 (*) g1) = (T2 . g2) (*) (T1 . g1) ) ) ) )