theorem Th4: :: CAT_4:4

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