let C be Category; :: thesis: for a being Object of C
for b being Object of (C opp) holds
( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) )
let a be Object of C; :: thesis: for b being Object of (C opp) holds
( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) )
let b be Object of (C opp); :: thesis: ( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) )
thus ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) :: thesis: ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f )

proof

assume A1: Hom ((a opp),b) <> {} ; :: thesis: for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f
A2: Hom ((opp b),(opp (a opp))) <> {} by A1, Th5;
let f be Morphism of a opp ,b; :: thesis: f (*) ((id a) opp) = f
A3: Hom (a,a) <> {} ;
A4: cod (opp f) = dom f
.= a by A1, CAT_1:5 ;
dom (opp f) = cod f
.= opp b by A1, CAT_1:5 ;
then reconsider ff = opp f as Morphism of opp b,a by A4, CAT_1:4;
A5: (id a) (*) ff = (id a) * ff by A3, A2, CAT_1:def 13;
thus f (*) ((id a) opp) = (ff opp) (*) ((id a) opp) by A2, Def6
.= ((id a) (*) ff) opp by A2, A3, Th14
.= ((id a) * ff) opp by A5, Def6, A2
.= ff opp by A2, CAT_1:28
.= f by A2, Def6 ; :: thesis: verum

end;

assume A6: Hom (b,(a opp)) <> {} ; :: thesis: for f being Morphism of b,a opp holds ((id a) opp) (*) f = f
A7: Hom ((opp (a opp)),(opp b)) <> {} by A6, Th5;
let f be Morphism of b,a opp ; :: thesis: ((id a) opp) (*) f = f
A8: Hom (a,a) <> {} ;
A9: dom (opp f) = cod f
.= a by A6, CAT_1:5 ;
cod (opp f) = dom f
.= opp b by A6, CAT_1:5 ;
then reconsider ff = opp f as Morphism of a, opp b by A9, CAT_1:4;
A10: ff (*) (id a) = ff * (id a) by A8, A7, CAT_1:def 13;
thus ((id a) opp) (*) f = ((id a) opp) (*) (ff opp) by A7, Def6
.= (ff (*) (id a)) opp by A8, A7, Th14
.= (ff * (id a)) opp by A10, Def6, A7
.= ff opp by A7, CAT_1:29
.= f by A7, Def6 ; :: thesis: verum