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