theorem Th35: :: CAT_3:35

for C being Category
for a, b being Object of C st b is terminal holds
( dom (term (a,b)) = a & cod (term (a,b)) = b )