theorem Th45: :: CAT_4:46

for o, m being set
for a, b being Object of (c1Cat* (o,m)) holds a = b