theorem Th16: :: CAT_3:16

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 doms F = I --> (cod f) holds
( doms (F * f) = I --> (dom f) & cods (F * f) = cods F )