theorem :: ENS_1:42

for C being Category
for a being Object of C
for f being Morphism of C holds
( ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) & ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) )