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