theorem Th9: :: CAT_1:11

for o, m being set
for a, b being Object of (1Cat (o,m))
for f being Morphism of (1Cat (o,m)) holds f in Hom (a,b)