for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C holds (id G) * F = id (G * F)