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 ;
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 ;
dom (opp f) = cod f
.= opp b by ;
then reconsider ff = opp f as Morphism of opp b,a by ;
A5: (id a) (*) ff = (id a) * ff by ;
thus f (*) ((id a) opp) = (ff opp) (*) ((id a) opp) by
.= ((id a) (*) ff) opp by A2, A3, Th14
.= ((id a) * ff) opp by A5, Def6, A2
.= ff opp by
.= f by ; :: 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 ;
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 ;
cod (opp f) = dom f
.= opp b by ;
then reconsider ff = opp f as Morphism of a, opp b by ;
A10: ff (*) (id a) = ff * (id a) by ;
thus ((id a) opp) (*) f = ((id a) opp) (*) (ff opp) by
.= (ff (*) (id a)) opp by A8, A7, Th14
.= (ff * (id a)) opp by
.= ff opp by
.= f by ; :: thesis: verum