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 )

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

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 A6:
Hom (b,(a opp)) <> {}
; :: thesis: for f being Morphism of b,a opp holds ((id a) opp) (*) f = f
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;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

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