theorem Th17: :: CAT_3:17

for I being set
for C being Category
for f being Morphism of C
for F being Function of I, the carrier' of C st cods F = I --> (dom f) holds
( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )