theorem Th55: :: CAT_8:55

for C1, C2 being category
for f1, g1 being morphism of C1
for f2, g2 being morphism of C2 st f1 |> g1 & f2 |> g2 holds
[f1,f2] (*) [g1,g2] = [(f1 (*) g1),(f2 (*) g2)]