for C being non empty category
for a1, a2 being Morphism of (Alter C)
for f1, f2 being morphism of C st a1 = f1 & a2 = f2 & f1 |> f2 holds
a1 (*) a2 = f1 (*) f2