for A, B being Category
for F being Functor of A,B
for a being Object of A holds F /. (id a) = id (F . a)