theorem :: CAT_1:63

for C, D being Category
for T being Functor of C,D
for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by Def19;