for C being non empty category
for f1 being morphism of C
for a1 being Morphism of (Alter C) st a1 = f1 holds
( dom f1 = dom a1 & cod f1 = cod a1 )