theorem Th73: :: CAT_1:78

for C being Category holds Obj (id C) = id the carrier of C