theorem Th13: :: CAT_5:13

for C being Categorial Category
for f being Morphism of C holds
( dom f = f `11 & cod f = f `12 )