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: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