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