theorem :: CAT_8:12

for C1, C2 being with_identities CategoryStr
for f being morphism of C1
for F being Functor of C1,C2 st F is covariant & f is identity holds
F . f is identity by CAT_6:def 22, CAT_6:def 25;