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