theorem Th31: :: ISOCAT_1:33

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