let C be Category; :: thesis: for a, b being Object of
for f being Morphism of holds
( f in Hom a,b iff opp f in Hom (opp b),(opp a) )
let a, b be Object of ; :: thesis: for f being Morphism of holds
( f in Hom a,b iff opp f in Hom (opp b),(opp a) )
let f be Morphism of ; :: thesis: ( f in Hom a,b iff opp f in Hom (opp b),(opp a) )
A1: ( f in Hom a,b iff ( dom f = a & cod f = b ) ) by CAT_1:18;
( dom (opp f) = cod f & cod (opp f) = dom f ) ;
hence ( f in Hom a,b iff opp f in Hom (opp b),(opp a) ) by A1, CAT_1:18; :: thesis: verum