for A being Category
for a1, a2 being Morphism of A
for f1, f2 being morphism of (alter A) st a1 = f1 & a2 = f2 & [a1,a2] in dom the Comp of A holds
a1 (*) a2 = f1 (*) f2