theorem Th2: :: NATTRA_1:6

for m, o being set holds the Comp of (1Cat (o,m)) = {[[m,m],m]}