let C be Category; :: thesis: for a, b being Object of C holds Hom (a,b) = Hom ((b opp),(a opp))

let a, b be Object of C; :: thesis: Hom (a,b) = Hom ((b opp),(a opp))

thus Hom (a,b) c= Hom ((b opp),(a opp)) :: according to XBOOLE_0:def 10 :: thesis: Hom ((b opp),(a opp)) c= Hom (a,b)

assume A2: x in Hom ((b opp),(a opp)) ; :: thesis: x in Hom (a,b)

then reconsider f = x as Morphism of (C opp) ;

reconsider g = f as Morphism of C ;

( dom f = b opp & cod f = a opp ) by A2, CAT_1:1;

then ( dom g = a & cod g = b ) ;

hence x in Hom (a,b) ; :: thesis: verum

let a, b be Object of C; :: thesis: Hom (a,b) = Hom ((b opp),(a opp))

thus Hom (a,b) c= Hom ((b opp),(a opp)) :: according to XBOOLE_0:def 10 :: thesis: Hom ((b opp),(a opp)) c= Hom (a,b)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Hom ((b opp),(a opp)) or x in Hom (a,b) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Hom (a,b) or x in Hom ((b opp),(a opp)) )

assume A1: x in Hom (a,b) ; :: thesis: x in Hom ((b opp),(a opp))

then reconsider f = x as Morphism of C ;

reconsider g = f as Morphism of (C opp) ;

( dom f = a & cod f = b ) by A1, CAT_1:1;

then ( dom g = b opp & cod g = a opp ) ;

hence x in Hom ((b opp),(a opp)) ; :: thesis: verum

end;assume A1: x in Hom (a,b) ; :: thesis: x in Hom ((b opp),(a opp))

then reconsider f = x as Morphism of C ;

reconsider g = f as Morphism of (C opp) ;

( dom f = a & cod f = b ) by A1, CAT_1:1;

then ( dom g = b opp & cod g = a opp ) ;

hence x in Hom ((b opp),(a opp)) ; :: thesis: verum

assume A2: x in Hom ((b opp),(a opp)) ; :: thesis: x in Hom (a,b)

then reconsider f = x as Morphism of (C opp) ;

reconsider g = f as Morphism of C ;

( dom f = b opp & cod f = a opp ) by A2, CAT_1:1;

then ( dom g = a & cod g = b ) ;

hence x in Hom (a,b) ; :: thesis: verum