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