let C be Category; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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:19;
hence ( ( Hom a,(cod f) = {} implies Hom a,(dom f) = {} ) & ( Hom (dom f),a = {} implies Hom (cod f),a = {} ) ) by CAT_1:52; :: thesis: verum