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 )
assume A1: Hom C c= V ; :: thesis: hom?? C is Functor of [:(C opp ),C:], Ens V
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 #) by OPPCAT_1:def 1;
then ( the carrier' of [:(C opp ),C:] = the carrier' of [:C,C:] & Maps (Hom C) c= Maps V & the carrier' of (Ens V) = Maps V & Maps (Hom C) <> {} ) by A1, Th7;
then reconsider T = hom?? C as Function of the carrier' of [:(C opp ),C:],the carrier' of (Ens V) by FUNCT_2:9;
A2: 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;

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:9;
Hom (opp a),b in Hom C ;
then reconsider A = Hom (opp a),b as Element of V by A1;
take d = @ A; :: thesis: T . (id c) = id d

now

thus id c = [(id a),(id b)] by A4, CAT_2:41
.= [(opp (id a)),(id b)] by A2
.= [(id (opp a)),(id b)] by OPPCAT_1:22 ; :: thesis: d = A
thus d = A ; :: thesis: verum

end;

hence T . (id c) = id d by A1, 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: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 A1;
set h = T . fg;
opp f = f by A2;
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 A2
.= 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 A1, 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:38
.= T . [(id (cod f)),(id (cod g))] by CAT_2:41
.= T . [(opp (id (cod f))),(id (cod g))] by A2
.= 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 A1, 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 f being Morphism of (C opp ), f' being Morphism of C such that
A8: ff = [f,f'] by DOMAIN_1:9;
consider g being Morphism of (C opp ), g' being Morphism of C such that
A9: gg = [g,g'] by DOMAIN_1:9;
opp f = f by A2;
then [[(Hom (cod (opp f)),(dom f')),(Hom (dom (opp f)),(cod f'))],(hom (opp f),f')] = @ (T . ff) by A8, 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 A10: ( (@ (T . ff)) `2 = hom (opp f),f' & dom (T . ff) = Hom (cod (opp f)),(dom f') & cod (T . ff) = Hom (dom (opp f)),(cod f') ) by Lm1, ZFMISC_1:33;
then A11: ( dom (@ (T . ff)) = Hom (cod (opp f)),(dom f') & cod (@ (T . ff)) = Hom (dom (opp f)),(cod f') ) by Def10, Def11;
opp g = g by A2;
then [[(Hom (cod (opp g)),(dom g')),(Hom (dom (opp g)),(cod g'))],(hom (opp g),g')] = @ (T . gg) by A9, 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 A12: ( (@ (T . gg)) `2 = hom (opp g),g' & dom (T . gg) = Hom (cod (opp g)),(dom g') & cod (T . gg) = Hom (dom (opp g)),(cod g') ) by Lm1, ZFMISC_1:33;
then A13: ( dom (@ (T . gg)) = Hom (cod (opp g)),(dom g') & cod (@ (T . gg)) = Hom (dom (opp g)),(cod g') ) by Def10, Def11;
A14: ( dom gg = [(dom g),(dom g')] & cod ff = [(cod f),(cod f')] ) by A8, A9, CAT_2:38;
then A15: dom g = cod f by A7, ZFMISC_1:33;

now

thus dom gg = [(opp (dom g)),(dom g')] by A3, A14
.= [(cod (opp g)),(dom g')] by OPPCAT_1:12 ; :: thesis: cod ff = [(dom (opp f)),(cod f')]
thus cod ff = [(opp (cod f)),(cod f')] by A3, A14
.= [(dom (opp f)),(cod f')] by OPPCAT_1:12 ; :: thesis: verum

end;

then A16: ( cod (opp g) = dom (opp f) & dom g' = cod f' ) by A7, ZFMISC_1:33;
then A17: ( dom (g' * f') = dom f' & cod (g' * f') = cod g' & dom ((opp f) * (opp g)) = dom (opp g) & cod ((opp f) * (opp g)) = cod (opp f) ) by CAT_1:42;
thus T . (gg * ff) = T . [(g * f),(g' * f')] by A7, A8, A9, CAT_2:40
.= T . [(opp (g * f)),(g' * f')] by A2
.= T . [((opp f) * (opp g)),(g' * f')] by A15, 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 A16, A17, Th56
.= (@ (T . gg)) * (@ (T . ff)) by A10, A11, A12, A13, A16, Def7
.= (T . gg) * (T . ff) by A10, A12, A16, Th28 ; :: thesis: verum

end;

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