theorem Th4: :: CAT_3:4

for I being set
for C being Category
for f being Morphism of C holds doms (I --> f) = I --> (dom f)