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