let V be non empty set ; :: thesis: for C being Category

for a being Object of C st Hom C c= V holds

hom-? a is Contravariant_Functor of C, Ens V

let C be Category; :: thesis: for a being Object of C st Hom C c= V holds

hom-? a is Contravariant_Functor of C, Ens V

let a be Object of C; :: thesis: ( Hom C c= V implies hom-? a is Contravariant_Functor of C, Ens V )

assume A1: Hom C c= V ; :: thesis: hom-? a is Contravariant_Functor of C, Ens V

then reconsider T = hom-? a as Function of the carrier' of C, the carrier' of (Ens V) by Lm8;

for a being Object of C st Hom C c= V holds

hom-? a is Contravariant_Functor of C, Ens V

let C be Category; :: thesis: for a being Object of C st Hom C c= V holds

hom-? a is Contravariant_Functor of C, Ens V

let a be Object of C; :: thesis: ( Hom C c= V implies hom-? a is Contravariant_Functor of C, Ens V )

assume A1: Hom C c= V ; :: thesis: hom-? a is Contravariant_Functor of C, Ens V

then reconsider T = hom-? a as Function of the carrier' of C, the carrier' of (Ens V) by Lm8;

now :: thesis: ( ( for c being Object of C ex d being Object of (Ens V) st T . (id c) = id d ) & ( for f being Morphism of C holds

( T . (id (dom f)) = id (cod (T . f)) & T . (id (cod f)) = id (dom (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

T . (g (*) f) = (T . f) (*) (T . g) ) )

hence
hom-? a is Contravariant_Functor of C, Ens V
by OPPCAT_1:def 9; :: thesis: verum( T . (id (dom f)) = id (cod (T . f)) & T . (id (cod f)) = id (dom (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

T . (g (*) f) = (T . f) (*) (T . g) ) )

thus
for c being Object of C ex d being Object of (Ens V) st T . (id c) = id d
:: thesis: ( ( for f being Morphism of C holds

( T . (id (dom f)) = id (cod (T . f)) & T . (id (cod f)) = id (dom (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

T . (g (*) f) = (T . f) (*) (T . g) ) )

( T . (id (dom f)) = id (cod (T . f)) & T . (id (cod f)) = id (dom (T . f)) ) :: thesis: for f, g being Morphism of C st dom g = cod f holds

T . (g (*) f) = (T . f) (*) (T . g)

assume A3: dom g = cod f ; :: thesis: T . (g (*) f) = (T . f) (*) (T . g)

A4: [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] = @ (T . g) by Def21

.= [[(dom (@ (T . g))),(cod (@ (T . g)))],((@ (T . g)) `2)] by Th8

.= [[(dom (T . g)),(cod (@ (T . g)))],((@ (T . g)) `2)] by Def9

.= [[(dom (T . g)),(cod (T . g))],((@ (T . g)) `2)] by Def10 ;

then A5: (@ (T . g)) `2 = hom (g,a) by XTUPLE_0:1;

dom (T . g) = Hom ((cod g),a) by A4, Lm1;

then A6: dom (@ (T . g)) = Hom ((cod g),a) by Def9;

A7: cod (T . g) = Hom ((dom g),a) by A4, Lm1;

then A8: cod (@ (T . g)) = Hom ((dom g),a) by Def10;

A9: [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] = @ (T . f) by Def21

.= [[(dom (@ (T . f))),(cod (@ (T . f)))],((@ (T . f)) `2)] by Th8

.= [[(dom (T . f)),(cod (@ (T . f)))],((@ (T . f)) `2)] by Def9

.= [[(dom (T . f)),(cod (T . f))],((@ (T . f)) `2)] by Def10 ;

then A10: (@ (T . f)) `2 = hom (f,a) by XTUPLE_0:1;

cod (T . f) = Hom ((dom f),a) by A9, Lm1;

then A11: cod (@ (T . f)) = Hom ((dom f),a) by Def10;

A12: dom (T . f) = Hom ((cod f),a) by A9, Lm1;

then A13: dom (@ (T . f)) = Hom ((cod f),a) by Def9;

( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A3, CAT_1:17;

hence T . (g (*) f) = [[(Hom ((cod g),a)),(Hom ((dom f),a))],(hom ((g (*) f),a))] by Def21

.= [[(Hom ((cod g),a)),(Hom ((dom f),a))],((hom (f,a)) * (hom (g,a)))] by A3, Th45

.= (@ (T . f)) * (@ (T . g)) by A3, A10, A13, A11, A5, A6, A8, Def6

.= (T . f) (*) (T . g) by A3, A12, A7, Th27 ;

:: thesis: verum

end;( T . (id (dom f)) = id (cod (T . f)) & T . (id (cod f)) = id (dom (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

T . (g (*) f) = (T . f) (*) (T . g) ) )

proof

thus
for f being Morphism of C holds
let c be Object of C; :: thesis: ex d being Object of (Ens V) st T . (id c) = id d

Hom (c,a) in Hom C ;

then reconsider A = Hom (c,a) as Element of V by A1;

take d = @ A; :: thesis: T . (id c) = id d

thus T . (id c) = id d by A1, Lm10; :: thesis: verum

end;Hom (c,a) in Hom C ;

then reconsider A = Hom (c,a) as Element of V by A1;

take d = @ A; :: thesis: T . (id c) = id d

thus T . (id c) = id d by A1, Lm10; :: thesis: verum

( T . (id (dom f)) = id (cod (T . f)) & T . (id (cod f)) = id (dom (T . f)) ) :: thesis: for f, g being Morphism of C st dom g = cod f holds

T . (g (*) f) = (T . f) (*) (T . g)

proof

let f, g be Morphism of C; :: thesis: ( dom g = cod f implies T . (g (*) f) = (T . f) (*) (T . g) )
let f be Morphism of C; :: thesis: ( T . (id (dom f)) = id (cod (T . f)) & T . (id (cod f)) = id (dom (T . f)) )

set b = cod f;

set c = dom f;

set g = T . f;

( Hom ((cod f),a) in Hom C & Hom ((dom f),a) in Hom C ) ;

then reconsider A = Hom ((cod f),a), B = Hom ((dom f),a) as Element of V by A1;

A2: [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] = @ (T . f) by Def21

.= [[(dom (@ (T . f))),(cod (@ (T . f)))],((@ (T . f)) `2)] by Th8

.= [[(dom (T . f)),(cod (@ (T . f)))],((@ (T . f)) `2)] by Def9

.= [[(dom (T . f)),(cod (T . f))],((@ (T . f)) `2)] by Def10 ;

thus T . (id (dom f)) = id (@ B) by A1, Lm10

.= id (cod (T . f)) by A2, Lm1 ; :: thesis: T . (id (cod f)) = id (dom (T . f))

thus T . (id (cod f)) = id (@ A) by A1, Lm10

.= id (dom (T . f)) by A2, Lm1 ; :: thesis: verum

end;set b = cod f;

set c = dom f;

set g = T . f;

( Hom ((cod f),a) in Hom C & Hom ((dom f),a) in Hom C ) ;

then reconsider A = Hom ((cod f),a), B = Hom ((dom f),a) as Element of V by A1;

A2: [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] = @ (T . f) by Def21

.= [[(dom (@ (T . f))),(cod (@ (T . f)))],((@ (T . f)) `2)] by Th8

.= [[(dom (T . f)),(cod (@ (T . f)))],((@ (T . f)) `2)] by Def9

.= [[(dom (T . f)),(cod (T . f))],((@ (T . f)) `2)] by Def10 ;

thus T . (id (dom f)) = id (@ B) by A1, Lm10

.= id (cod (T . f)) by A2, Lm1 ; :: thesis: T . (id (cod f)) = id (dom (T . f))

thus T . (id (cod f)) = id (@ A) by A1, Lm10

.= id (dom (T . f)) by A2, Lm1 ; :: thesis: verum

assume A3: dom g = cod f ; :: thesis: T . (g (*) f) = (T . f) (*) (T . g)

A4: [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] = @ (T . g) by Def21

.= [[(dom (@ (T . g))),(cod (@ (T . g)))],((@ (T . g)) `2)] by Th8

.= [[(dom (T . g)),(cod (@ (T . g)))],((@ (T . g)) `2)] by Def9

.= [[(dom (T . g)),(cod (T . g))],((@ (T . g)) `2)] by Def10 ;

then A5: (@ (T . g)) `2 = hom (g,a) by XTUPLE_0:1;

dom (T . g) = Hom ((cod g),a) by A4, Lm1;

then A6: dom (@ (T . g)) = Hom ((cod g),a) by Def9;

A7: cod (T . g) = Hom ((dom g),a) by A4, Lm1;

then A8: cod (@ (T . g)) = Hom ((dom g),a) by Def10;

A9: [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] = @ (T . f) by Def21

.= [[(dom (@ (T . f))),(cod (@ (T . f)))],((@ (T . f)) `2)] by Th8

.= [[(dom (T . f)),(cod (@ (T . f)))],((@ (T . f)) `2)] by Def9

.= [[(dom (T . f)),(cod (T . f))],((@ (T . f)) `2)] by Def10 ;

then A10: (@ (T . f)) `2 = hom (f,a) by XTUPLE_0:1;

cod (T . f) = Hom ((dom f),a) by A9, Lm1;

then A11: cod (@ (T . f)) = Hom ((dom f),a) by Def10;

A12: dom (T . f) = Hom ((cod f),a) by A9, Lm1;

then A13: dom (@ (T . f)) = Hom ((cod f),a) by Def9;

( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A3, CAT_1:17;

hence T . (g (*) f) = [[(Hom ((cod g),a)),(Hom ((dom f),a))],(hom ((g (*) f),a))] by Def21

.= [[(Hom ((cod g),a)),(Hom ((dom f),a))],((hom (f,a)) * (hom (g,a)))] by A3, Th45

.= (@ (T . f)) * (@ (T . g)) by A3, A10, A13, A11, A5, A6, A8, Def6

.= (T . f) (*) (T . g) by A3, A12, A7, Th27 ;

:: thesis: verum