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