theorem Th5: :: CAT_2:9
for C being Category
for E being Subcategory of C
for f being Morphism of E
for f9 being Morphism of C st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )