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;

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) ) )

hence
hom?? C is Functor of [:(C opp),C:], Ens V
by CAT_1:61; :: thesis: verum( 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) ) )

( 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)

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;( 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

thus
for fg being Morphism of [:(C opp),C:] holds
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;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

( 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 ff, gg be Morphism of [:(C opp),C:]; :: thesis: ( dom gg = cod ff implies T . (gg (*) ff) = (T . gg) (*) (T . ff) )
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;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

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