theorem :: CAT_6:33

for C, D being non empty composable with_identities CategoryStr
for F being covariant Functor of C,D
for o being Object of C holds F . (id- o) = id- (F . o) by Def21;