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

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