theorem Th51: :: CAT_8:51

for C1, C2 being category holds (id C1) [x] (id C2) = id (C1 [x] C2)