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:2;

hence ( ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) & ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) ) by CAT_1:24; :: thesis: verum

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:2;

hence ( ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) & ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) ) by CAT_1:24; :: thesis: verum