for C, D, E being with_identities CategoryStr
for F being Functor of C,D
for G being Functor of D,E
for f being morphism of C st F is covariant & G is covariant & not C is empty holds
(G (*) F) . f = G . (F . f)