for o, m being set
for f, g being Morphism of (c1Cat (o,m)) holds f = g