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

now

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

proof

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, Lm9; :: thesis: verum

end;

thus for f being Morphism of C holds
( 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 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;
( 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;
set g = T . f;
A2: [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] = @ (T . f) by Def23
.= [[(dom (@ (T . f))),(cod (@ (T . f)))],((@ (T . f)) `2 )] by Th8
.= [[(dom (T . f)),(cod (@ (T . f)))],((@ (T . f)) `2 )] by Def10
.= [[(dom (T . f)),(cod (T . f))],((@ (T . f)) `2 )] by Def11 ;
thus T . (id (dom f)) = id (@ B) by A1, Lm9
.= 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, Lm9
.= id (dom (T . f)) by A2, Lm1 ; :: thesis: verum

end;

let f, g be Morphism of C; :: thesis: ( dom g = cod f implies T . (g * f) = (T . f) * (T . g) )
assume A3: dom g = cod f ; :: thesis: T . (g * f) = (T . f) * (T . g)
[[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] = @ (T . f) by Def23
.= [[(dom (@ (T . f))),(cod (@ (T . f)))],((@ (T . f)) `2 )] by Th8
.= [[(dom (T . f)),(cod (@ (T . f)))],((@ (T . f)) `2 )] by Def10
.= [[(dom (T . f)),(cod (T . f))],((@ (T . f)) `2 )] by Def11 ;
then A4: ( (@ (T . f)) `2 = hom f,a & dom (T . f) = Hom (cod f),a & cod (T . f) = Hom (dom f),a ) by Lm1, ZFMISC_1:33;
then A5: ( dom (@ (T . f)) = Hom (cod f),a & cod (@ (T . f)) = Hom (dom f),a ) by Def10, Def11;
[[(Hom (cod g),a),(Hom (dom g),a)],(hom g,a)] = @ (T . g) by Def23
.= [[(dom (@ (T . g))),(cod (@ (T . g)))],((@ (T . g)) `2 )] by Th8
.= [[(dom (T . g)),(cod (@ (T . g)))],((@ (T . g)) `2 )] by Def10
.= [[(dom (T . g)),(cod (T . g))],((@ (T . g)) `2 )] by Def11 ;
then A6: ( (@ (T . g)) `2 = hom g,a & dom (T . g) = Hom (cod g),a & cod (T . g) = Hom (dom g),a ) by Lm1, ZFMISC_1:33;
then A7: ( dom (@ (T . g)) = Hom (cod g),a & cod (@ (T . g)) = Hom (dom g),a ) by Def10, Def11;
( dom (g * f) = dom f & cod (g * f) = cod g ) by A3, CAT_1:42;
hence T . (g * f) = [[(Hom (cod g),a),(Hom (dom f),a)],(hom (g * f),a)] by Def23
.= [[(Hom (cod g),a),(Hom (dom f),a)],((hom f,a) * (hom g,a))] by A3, Th46
.= (@ (T . f)) * (@ (T . g)) by A3, A4, A5, A6, A7, Def7
.= (T . f) * (T . g) by A3, A4, A6, Th28 ;
:: thesis: verum

end;

hence hom-? a is Contravariant_Functor of C, Ens V by OPPCAT_1:def 7; :: thesis: verum