let C be Category; :: thesis: for f, f9 being Morphism of C st Hom (dom f),(cod f9) = {} holds
Hom (cod f),(dom f9) = {}
let f, f9 be Morphism of C; :: thesis: ( Hom (dom f),(cod f9) = {} implies Hom (cod f),(dom f9) = {} )
assume that
A1: Hom (dom f),(cod f9) = {} and
A2: Hom (cod f),(dom f9) <> {} ; :: thesis: contradiction
A3: Hom (dom f9),(cod f9) <> {} by CAT_1:19;
Hom (dom f),(cod f) <> {} by CAT_1:19;
then Hom (dom f),(dom f9) <> {} by A2, CAT_1:52;
hence contradiction by A1, A3, CAT_1:52; :: thesis: verum