let V be non empty set ; :: thesis: for C being Category st Hom C c= V holds
hom?? C is Functor of [:(C opp),C:], Ens V
let C be Category; :: thesis: ( Hom C c= V implies hom?? C is Functor of [:(C opp),C:], Ens V )
A1: for f being Morphism of (C opp) holds opp f = f

proof

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

end;

assume A2: Hom C c= V ; :: thesis: hom?? C is Functor of [:(C opp),C:], Ens V
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:7;
A3: for a being Object of (C opp) holds opp a = a

proof

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

end;

now

thus for c being Object of [:(C opp),C:] ex d being Object of (Ens V) st T . (id c) = id d :: thesis: ( ( for fg being Morphism of [:(C opp),C:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for ff, gg being Morphism of [:(C opp),C:] st dom gg = cod ff holds
T . (gg * ff) = (T . gg) * (T . ff) ) )

proof

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

end;

thus for fg being Morphism of [:(C opp),C:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) :: thesis: for ff, gg being Morphism of [:(C opp),C:] st dom gg = cod ff holds
T . (gg * ff) = (T . gg) * (T . ff)

proof

let fg be Morphism of [:(C opp),C:]; :: thesis: ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) )
consider f being Morphism of (C opp), g being Morphism of C such that
A5: fg = [f,g] by DOMAIN_1:1;
( 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:28
.= T . [(id (dom f)),(id (dom g))] by CAT_2:31
.= T . [(opp (id (dom f))),(id (dom g))] by A1
.= T . [(id (opp (dom f))),(id (dom g))] by OPPCAT_1:21
.= T . [(id (cod (opp f))),(id (dom g))] by OPPCAT_1:11
.= id (@ A) by A2, Lm10
.= id (dom (T . fg)) by A6, Lm1 ; :: thesis: T . (id (cod fg)) = id (cod (T . fg))
thus T . (id (cod fg)) = T . (id [(cod f),(cod g)]) by A5, CAT_2:28
.= T . [(id (cod f)),(id (cod g))] by CAT_2:31
.= T . [(opp (id (cod f))),(id (cod g))] by A1
.= T . [(id (opp (cod f))),(id (cod g))] by OPPCAT_1:21
.= T . [(id (dom (opp f))),(id (cod g))] by OPPCAT_1:11
.= id (@ B) by A2, Lm10
.= id (cod (T . fg)) by A6, Lm1 ; :: thesis: verum

end;

let ff, gg be Morphism of [:(C opp),C:]; :: thesis: ( dom gg = cod ff implies T . (gg * ff) = (T . gg) * (T . ff) )
assume A7: dom gg = cod ff ; :: thesis: T . (gg * ff) = (T . gg) * (T . ff)
consider g being Morphism of (C opp), g9 being Morphism of C such that
A8: gg = [g,g9] by DOMAIN_1:1;
opp g = g by A1;
then A9: [[(Hom ((cod (opp g)),(dom g9))),(Hom ((dom (opp g)),(cod g9)))],(hom ((opp g),g9))] = @ (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),g9) by ZFMISC_1:27;
cod (T . gg) = Hom ((dom (opp g)),(cod g9)) by A9, Lm1;
then A11: cod (@ (T . gg)) = Hom ((dom (opp g)),(cod g9)) by Def11;
A12: dom (T . gg) = Hom ((cod (opp g)),(dom g9)) by A9, Lm1;
then A13: dom (@ (T . gg)) = Hom ((cod (opp g)),(dom g9)) by Def10;
consider f being Morphism of (C opp), f9 being Morphism of C such that
A14: ff = [f,f9] by DOMAIN_1:1;
opp f = f by A1;
then A15: [[(Hom ((cod (opp f)),(dom f9))),(Hom ((dom (opp f)),(cod f9)))],(hom ((opp f),f9))] = @ (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),f9) by ZFMISC_1:27;
dom (T . ff) = Hom ((cod (opp f)),(dom f9)) by A15, Lm1;
then A17: dom (@ (T . ff)) = Hom ((cod (opp f)),(dom f9)) by Def10;
A18: cod (T . ff) = Hom ((dom (opp f)),(cod f9)) by A15, Lm1;
then A19: cod (@ (T . ff)) = Hom ((dom (opp f)),(cod f9)) by Def11;
A20: cod ff = [(cod f),(cod f9)] by A14, CAT_2:28;
then A21: cod ff = [(opp (cod f)),(cod f9)] by A3
.= [(dom (opp f)),(cod f9)] by OPPCAT_1:11 ;
A22: dom gg = [(dom g),(dom g9)] by A8, CAT_2:28;
then A23: dom gg = [(opp (dom g)),(dom g9)] by A3
.= [(cod (opp g)),(dom g9)] by OPPCAT_1:11 ;
then A24: cod (opp g) = dom (opp f) by A7, A21, ZFMISC_1:27;
then A25: ( dom ((opp f) * (opp g)) = dom (opp g) & cod ((opp f) * (opp g)) = cod (opp f) ) by CAT_1:17;
A26: dom g = cod f by A7, A22, A20, ZFMISC_1:27;
A27: dom g9 = cod f9 by A7, A23, A21, ZFMISC_1:27;
then A28: ( dom (g9 * f9) = dom f9 & cod (g9 * f9) = cod g9 ) by CAT_1:17;
thus T . (gg * ff) = T . [(g * f),(g9 * f9)] by A7, A14, A8, CAT_2:30
.= T . [(opp (g * f)),(g9 * f9)] by A1
.= T . [((opp f) * (opp g)),(g9 * f9)] by A26, OPPCAT_1:18
.= [[(Hom ((cod ((opp f) * (opp g))),(dom (g9 * f9)))),(Hom ((dom ((opp f) * (opp g))),(cod (g9 * f9))))],(hom (((opp f) * (opp g)),(g9 * f9)))] by Def25
.= [[(Hom ((cod (opp f)),(dom f9))),(Hom ((dom (opp g)),(cod g9)))],((hom ((opp g),g9)) * (hom ((opp f),f9)))] 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: verum

end;

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