let C be 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) = {} ) )
let a be 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) = {} ) )
let f be Morphism of C; ( ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) & ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) )
Hom ((dom f),(cod f)) <> {}
by CAT_1:2;
hence
( ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) & ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) )
by CAT_1:24; verum