let C be Category; :: thesis: for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( dom (f opp) = cod f & cod (f opp) = dom f )
let a, b be Object of C; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds
( dom (f opp) = cod f & cod (f opp) = dom f ) )
assume A1: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds
( dom (f opp) = cod f & cod (f opp) = dom f )
then A2: Hom ((b opp),(a opp)) <> {} by Th4;
let f be Morphism of a,b; :: thesis: ( dom (f opp) = cod f & cod (f opp) = dom f )
thus dom (f opp) = b by A2, CAT_1:5
.= cod f by A1, CAT_1:5 ; :: thesis: cod (f opp) = dom f
thus cod (f opp) = a by A2, CAT_1:5
.= dom f by A1, CAT_1:5 ; :: thesis: verum