theorem Th50: :: ENS_1:51

for C being Category
for f, f9 being Morphism of C st Hom ((dom f),(cod f9)) = {} holds
Hom ((cod f),(dom f9)) = {}