let C be Category; :: thesis: for a, b being Object of (C opp)
for f being Morphism of (C opp) holds
( f in Hom (a,b) iff opp f in Hom ((opp b),(opp a)) )
let a, b be Object of (C opp); :: thesis: for f being Morphism of (C opp) holds
( f in Hom (a,b) iff opp f in Hom ((opp b),(opp a)) )
let f be Morphism of (C opp); :: 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:1;
( 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:1; :: thesis: verum