for C, D being non empty composable with_identities CategoryStr
for F being covariant Functor of C,D
for f being morphism of C holds
( F . (dom f) = dom (F . f) & F . (cod f) = cod (F . f) )