theorem Th30: :: ISOCAT_1:32

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)