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