let C be Category; 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; ( 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)) <> {}
; 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; verum