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:2;
Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then Hom ((dom f),(dom f9)) <> {} by A2, CAT_1:24;
hence contradiction by A1, A3, CAT_1:24; :: thesis: verum