theorem Th4: :: COMMACAT:4

for y, x being set
for a, b being Object of (1Cat (x,y)) holds Hom (a,b) = {y}