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
then ( C opp = CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) & Maps (Hom C) c= Maps V ) by Th7;
then reconsider T = hom?? C as Function of the carrier' of [:(C opp),C:], the carrier' of (Ens V) by FUNCT_2:7;

now :: thesis: ( ( for c being Object of [:(C opp),C:] ex d being Object of (Ens V) st T . (id c) = id d ) & ( 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) ) )

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
A2: 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 A1;
take d = @ A; :: thesis: T . (id c) = id d
A3: id (opp a) = id a by OPPCAT_1:72;
id c = [(id (opp a)),(id b)] by A3, A2, CAT_2:31;
hence T . (id c) = id d by A1, Lm11; :: 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
A4: 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 A1;
set h = T . fg;
A5: id (opp (dom f)) = id (dom f) by OPPCAT_1:72;
A6: id (opp (cod f)) = id (cod f) by OPPCAT_1:72;
A7: [[(Hom ((cod (opp f)),(dom g))),(Hom ((dom (opp f)),(cod g)))],(hom ((opp f),g))] = @ (T . fg) by A4, Def23
.= [[(dom (@ (T . fg))),(cod (@ (T . fg)))],((@ (T . fg)) `2)] by Th8
.= [[(dom (T . fg)),(cod (@ (T . fg)))],((@ (T . fg)) `2)] by Def9
.= [[(dom (T . fg)),(cod (T . fg))],((@ (T . fg)) `2)] by Def10 ;
thus T . (id (dom fg)) = T . (id [(dom f),(dom g)]) by A4, CAT_2:28
.= T . [(id (dom f)),(id (dom g))] by CAT_2:31
.= id (@ A) by A1, Lm11, A5
.= id (dom (T . fg)) by A7, Lm1 ; :: thesis: T . (id (cod fg)) = id (cod (T . fg))
thus T . (id (cod fg)) = T . (id [(cod f),(cod g)]) by A4, CAT_2:28
.= T . [(id (cod f)),(id (cod g))] by CAT_2:31
.= id (@ B) by A1, Lm11, A6
.= id (cod (T . fg)) by A7, 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 A8: 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
A9: gg = [g,g9] by DOMAIN_1:1;
A10: [[(Hom ((cod (opp g)),(dom g9))),(Hom ((dom (opp g)),(cod g9)))],(hom ((opp g),g9))] = @ (T . gg) by A9, Def23
.= [[(dom (@ (T . gg))),(cod (@ (T . gg)))],((@ (T . gg)) `2)] by Th8
.= [[(dom (T . gg)),(cod (@ (T . gg)))],((@ (T . gg)) `2)] by Def9
.= [[(dom (T . gg)),(cod (T . gg))],((@ (T . gg)) `2)] by Def10 ;
then A11: (@ (T . gg)) `2 = hom ((opp g),g9) by XTUPLE_0:1;
cod (T . gg) = Hom ((dom (opp g)),(cod g9)) by A10, Lm1;
then A12: cod (@ (T . gg)) = Hom ((dom (opp g)),(cod g9)) by Def10;
A13: dom (T . gg) = Hom ((cod (opp g)),(dom g9)) by A10, Lm1;
then A14: dom (@ (T . gg)) = Hom ((cod (opp g)),(dom g9)) by Def9;
consider f being Morphism of (C opp), f9 being Morphism of C such that
A15: ff = [f,f9] by DOMAIN_1:1;
A16: [[(Hom ((cod (opp f)),(dom f9))),(Hom ((dom (opp f)),(cod f9)))],(hom ((opp f),f9))] = @ (T . ff) by A15, Def23
.= [[(dom (@ (T . ff))),(cod (@ (T . ff)))],((@ (T . ff)) `2)] by Th8
.= [[(dom (T . ff)),(cod (@ (T . ff)))],((@ (T . ff)) `2)] by Def9
.= [[(dom (T . ff)),(cod (T . ff))],((@ (T . ff)) `2)] by Def10 ;
then A17: (@ (T . ff)) `2 = hom ((opp f),f9) by XTUPLE_0:1;
dom (T . ff) = Hom ((cod (opp f)),(dom f9)) by A16, Lm1;
then A18: dom (@ (T . ff)) = Hom ((cod (opp f)),(dom f9)) by Def9;
A19: cod (T . ff) = Hom ((dom (opp f)),(cod f9)) by A16, Lm1;
then A20: cod (@ (T . ff)) = Hom ((dom (opp f)),(cod f9)) by Def10;
A21: cod ff = [(cod f),(cod f9)] by A15, CAT_2:28;
A22: dom gg = [(dom g),(dom g9)] by A9, CAT_2:28;
then A23: cod (opp g) = dom (opp f) by A8, A21, XTUPLE_0:1;
then A24: ( dom ((opp f) (*) (opp g)) = dom (opp g) & cod ((opp f) (*) (opp g)) = cod (opp f) ) by CAT_1:17;
A25: dom g = cod f by A8, A22, A21, XTUPLE_0:1;
A26: dom g9 = cod f9 by A8, A22, A21, XTUPLE_0:1;
then A27: ( dom (g9 (*) f9) = dom f9 & cod (g9 (*) f9) = cod g9 ) by CAT_1:17;
thus T . (gg (*) ff) = T . [(opp (g (*) f)),(g9 (*) f9)] by A8, A15, A9, CAT_2:30
.= T . [((opp f) (*) (opp g)),(g9 (*) f9)] by A25, 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 Def23
.= [[(Hom ((cod (opp f)),(dom f9))),(Hom ((dom (opp g)),(cod g9)))],((hom ((opp g),g9)) * (hom ((opp f),f9)))] by A23, A26, A27, A24, Th55
.= (@ (T . gg)) * (@ (T . ff)) by A17, A18, A20, A11, A14, A12, A23, A26, Def6
.= (T . gg) (*) (T . ff) by A19, A13, A23, A26, Th27 ; :: thesis: verum

end;

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