let V be non empty set ; :: thesis:
let C be Category; :: thesis:
A1: for f being Morphism of holds opp f = f

let f be Morphism of ; :: thesis:
thus opp f = f opp by OPPCAT_1:def 5
.= f by OPPCAT_1:def 4 ; :: thesis:

end;

assume A2: Hom C c= V ; :: thesis:
then ( C opp = CatStr(# the carrier of C,the carrier' of C,the Target of C,the Source of C,(~ the Comp of C),the Id of C #) & Maps (Hom C) c= Maps V ) by Th7, OPPCAT_1:def 1;
then reconsider T = hom?? C as Function of the carrier' of [:(C opp ),C:],the carrier' of (Ens V) by FUNCT_2:9;
A3: for a being Object of holds opp a = a

proof

let a be Object of ; :: thesis:
thus opp a = a opp by OPPCAT_1:def 3
.= a by OPPCAT_1:def 2 ; :: thesis:

end;

now

thus for c being Object of ex d being Object of st T . (id c) = id d :: thesis:

proof

let c be Object of ; :: thesis:
consider a being Object of , b being Object of such that
A4: c = [a,b] by DOMAIN_1:9;
Hom (opp a),b in Hom C ;
then reconsider A = Hom (opp a),b as Element of V by A2;
take d = @ A; :: thesis:
id c = [(id a),(id b)] by A4, CAT_2:41
.= [(opp (id a)),(id b)] by A1
.= [(id (opp a)),(id b)] by OPPCAT_1:22 ;
hence T . (id c) = id d by A2, Lm10; :: thesis:

end;

thus for fg being Morphism of holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) :: thesis:

proof

let fg be Morphism of ; :: thesis:
consider f being Morphism of , g being Morphism of such that
A5: fg = [f,g] by DOMAIN_1:9;
( Hom (cod (opp f)),(dom g) in Hom C & Hom (dom (opp f)),(cod g) in Hom C ) ;
then reconsider A = Hom (cod (opp f)),(dom g), B = Hom (dom (opp f)),(cod g) as Element of V by A2;
set h = T . fg;
opp f = f by A1;
then A6: [[(Hom (cod (opp f)),(dom g)),(Hom (dom (opp f)),(cod g))],(hom (opp f),g)] = @ (T . fg) by A5, Def25
.= [[(dom (@ (T . fg))),(cod (@ (T . fg)))],((@ (T . fg)) `2 )] by Th8
.= [[(dom (T . fg)),(cod (@ (T . fg)))],((@ (T . fg)) `2 )] by Def10
.= [[(dom (T . fg)),(cod (T . fg))],((@ (T . fg)) `2 )] by Def11 ;
thus T . (id (dom fg)) = T . (id [(dom f),(dom g)]) by A5, CAT_2:38
.= T . [(id (dom f)),(id (dom g))] by CAT_2:41
.= T . [(opp (id (dom f))),(id (dom g))] by A1
.= T . [(id (opp (dom f))),(id (dom g))] by OPPCAT_1:22
.= T . [(id (cod (opp f))),(id (dom g))] by OPPCAT_1:12
.= id (@ A) by A2, Lm10
.= id (dom (T . fg)) by A6, Lm1 ; :: thesis:
thus T . (id (cod fg)) = T . (id [(cod f),(cod g)]) by A5, CAT_2:38
.= T . [(id (cod f)),(id (cod g))] by CAT_2:41
.= T . [(opp (id (cod f))),(id (cod g))] by A1
.= T . [(id (opp (cod f))),(id (cod g))] by OPPCAT_1:22
.= T . [(id (dom (opp f))),(id (cod g))] by OPPCAT_1:12
.= id (@ B) by A2, Lm10
.= id (cod (T . fg)) by A6, Lm1 ; :: thesis:

end;

let ff, gg be Morphism of ; :: thesis:
assume A7: dom gg = cod ff ; :: thesis:
consider g being Morphism of , g' being Morphism of such that
A8: gg = [g,g'] by DOMAIN_1:9;
opp g = g by A1;
then A9: [[(Hom (cod (opp g)),(dom g')),(Hom (dom (opp g)),(cod g'))],(hom (opp g),g')] = @ (T . gg) by A8, Def25
.= [[(dom (@ (T . gg))),(cod (@ (T . gg)))],((@ (T . gg)) `2 )] by Th8
.= [[(dom (T . gg)),(cod (@ (T . gg)))],((@ (T . gg)) `2 )] by Def10
.= [[(dom (T . gg)),(cod (T . gg))],((@ (T . gg)) `2 )] by Def11 ;
then A10: (@ (T . gg)) `2 = hom (opp g),g' by ZFMISC_1:33;
cod (T . gg) = Hom (dom (opp g)),(cod g') by A9, Lm1;
then A11: cod (@ (T . gg)) = Hom (dom (opp g)),(cod g') by Def11;
A12: dom (T . gg) = Hom (cod (opp g)),(dom g') by A9, Lm1;
then A13: dom (@ (T . gg)) = Hom (cod (opp g)),(dom g') by Def10;
consider f being Morphism of , f' being Morphism of such that
A14: ff = [f,f'] by DOMAIN_1:9;
opp f = f by A1;
then A15: [[(Hom (cod (opp f)),(dom f')),(Hom (dom (opp f)),(cod f'))],(hom (opp f),f')] = @ (T . ff) by A14, Def25
.= [[(dom (@ (T . ff))),(cod (@ (T . ff)))],((@ (T . ff)) `2 )] by Th8
.= [[(dom (T . ff)),(cod (@ (T . ff)))],((@ (T . ff)) `2 )] by Def10
.= [[(dom (T . ff)),(cod (T . ff))],((@ (T . ff)) `2 )] by Def11 ;
then A16: (@ (T . ff)) `2 = hom (opp f),f' by ZFMISC_1:33;
dom (T . ff) = Hom (cod (opp f)),(dom f') by A15, Lm1;
then A17: dom (@ (T . ff)) = Hom (cod (opp f)),(dom f') by Def10;
A18: cod (T . ff) = Hom (dom (opp f)),(cod f') by A15, Lm1;
then A19: cod (@ (T . ff)) = Hom (dom (opp f)),(cod f') by Def11;
A20: cod ff = [(cod f),(cod f')] by A14, CAT_2:38;
then A21: cod ff = [(opp (cod f)),(cod f')] by A3
.= [(dom (opp f)),(cod f')] by OPPCAT_1:12 ;
A22: dom gg = [(dom g),(dom g')] by A8, CAT_2:38;
then A23: dom gg = [(opp (dom g)),(dom g')] by A3
.= [(cod (opp g)),(dom g')] by OPPCAT_1:12 ;
then A24: cod (opp g) = dom (opp f) by A7, A21, ZFMISC_1:33;
then A25: ( dom ((opp f) * (opp g)) = dom (opp g) & cod ((opp f) * (opp g)) = cod (opp f) ) by CAT_1:42;
A26: dom g = cod f by A7, A22, A20, ZFMISC_1:33;
A27: dom g' = cod f' by A7, A23, A21, ZFMISC_1:33;
then A28: ( dom (g' * f') = dom f' & cod (g' * f') = cod g' ) by CAT_1:42;
thus T . (gg * ff) = T . [(g * f),(g' * f')] by A7, A14, A8, CAT_2:40
.= T . [(opp (g * f)),(g' * f')] by A1
.= T . [((opp f) * (opp g)),(g' * f')] by A26, OPPCAT_1:19
.= [[(Hom (cod ((opp f) * (opp g))),(dom (g' * f'))),(Hom (dom ((opp f) * (opp g))),(cod (g' * f')))],(hom ((opp f) * (opp g)),(g' * f'))] by Def25
.= [[(Hom (cod (opp f)),(dom f')),(Hom (dom (opp g)),(cod g'))],((hom (opp g),g') * (hom (opp f),f'))] by A24, A27, A28, A25, Th56
.= (@ (T . gg)) * (@ (T . ff)) by A16, A17, A19, A10, A13, A11, A24, A27, Def7
.= (T . gg) * (T . ff) by A18, A12, A24, A27, Th28 ; :: thesis:

end;

hence hom?? C is Functor of [:(C opp ),C:], Ens V by CAT_1:96; :: thesis: