:: ENS_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let V be non empty set ;
func Funcs V -> set equals :: ENS_1:def 1
union { (Funcs A,B) where A, B is Element of V : verum } ;
coherence
union { (Funcs A,B) where A, B is Element of V : verum } is set
;
end;

:: deftheorem defines Funcs ENS_1:def 1 :
for V being non empty set holds Funcs V = union { (Funcs A,B) where A, B is Element of V : verum } ;

registration
let V be non empty set ;
cluster Funcs V -> non empty functional ;
coherence
( Funcs V is functional & not Funcs V is empty )
proof end;
end;

theorem Th1: :: ENS_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for f being set holds
( f in Funcs V iff ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B ) )
proof end;

theorem :: ENS_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for A, B being Element of V holds Funcs A,B c= Funcs V
proof end;

theorem Th3: :: ENS_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for W being non empty Subset of V holds Funcs W c= Funcs V
proof end;

definition
let V be non empty set ;
func Maps V -> set equals :: ENS_1:def 2
{ [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } ;
coherence
{ [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } is set
;
end;

:: deftheorem defines Maps ENS_1:def 2 :
for V being non empty set holds Maps V = { [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } ;

registration
let V be non empty set ;
cluster Maps V -> non empty ;
coherence
not Maps V is empty
proof end;
end;

theorem Th4: :: ENS_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for m being Element of Maps V ex f being Element of Funcs V ex A, B being Element of V st
( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B )
proof end;

theorem Th5: :: ENS_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for A, B being Element of V
for f being Function of A,B st ( B = {} implies A = {} ) holds
[[A,B],f] in Maps V
proof end;

theorem :: ENS_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set holds Maps V c= [:[:V,V:],(Funcs V):]
proof end;

theorem Th7: :: ENS_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for W being non empty Subset of V holds Maps W c= Maps V
proof end;

Lm1: for x1, y1, x2, y2, x3, y3 being set st [[x1,x2],x3] = [[y1,y2],y3] holds
( x1 = y1 & x2 = y2 )
proof end;

registration
let V be non empty set ;
let m be Element of Maps V;
cluster m `2 -> Relation-like Function-like ;
coherence
( m `2 is Function-like & m `2 is Relation-like )
proof end;
end;

definition
let V be non empty set ;
let m be Element of Maps V;
canceled;
func dom m -> Element of V equals :: ENS_1:def 4
(m `1 ) `1 ;
coherence
(m `1 ) `1 is Element of V
proof end;
func cod m -> Element of V equals :: ENS_1:def 5
(m `1 ) `2 ;
coherence
(m `1 ) `2 is Element of V
proof end;
end;

:: deftheorem ENS_1:def 3 :
canceled;

:: deftheorem defines dom ENS_1:def 4 :
for V being non empty set
for m being Element of Maps V holds dom m = (m `1 ) `1 ;

:: deftheorem defines cod ENS_1:def 5 :
for V being non empty set
for m being Element of Maps V holds cod m = (m `1 ) `2 ;

theorem Th8: :: ENS_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for m being Element of Maps V holds m = [[(dom m),(cod m)],(m `2 )]
proof end;

Lm2: for V being non empty set
for m, m' being Element of Maps V st m `2 = m' `2 & dom m = dom m' & cod m = cod m' holds
m = m'
proof end;

theorem Th9: :: ENS_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for m being Element of Maps V holds
( ( cod m <> {} or dom m = {} ) & m `2 is Function of dom m, cod m )
proof end;

Lm3: for V being non empty set
for m being Element of Maps V holds
( dom (m `2 ) = dom m & rng (m `2 ) c= cod m )
proof end;

theorem Th10: :: ENS_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for f being Function
for A, B being set st [[A,B],f] in Maps V holds
( ( B = {} implies A = {} ) & f is Function of A,B )
proof end;

definition
let V be non empty set ;
let A be Element of V;
func id$ A -> Element of Maps V equals :: ENS_1:def 6
[[A,A],(id A)];
coherence
[[A,A],(id A)] is Element of Maps V
proof end;
end;

:: deftheorem defines id$ ENS_1:def 6 :
for V being non empty set
for A being Element of V holds id$ A = [[A,A],(id A)];

theorem Th11: :: ENS_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for A being Element of V holds
( (id$ A) `2 = id A & dom (id$ A) = A & cod (id$ A) = A )
proof end;

definition
let V be non empty set ;
let m1, m2 be Element of Maps V;
assume A1: cod m1 = dom m2 ;
func m2 * m1 -> Element of Maps V equals :Def7: :: ENS_1:def 7
[[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))];
coherence
[[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))] is Element of Maps V
proof end;
end;

:: deftheorem Def7 defines * ENS_1:def 7 :
for V being non empty set
for m1, m2 being Element of Maps V st cod m1 = dom m2 holds
m2 * m1 = [[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))];

theorem Th12: :: ENS_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
( (m2 * m1) `2 = (m2 `2 ) * (m1 `2 ) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 )
proof end;

theorem Th13: :: ENS_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for m2, m1, m3 being Element of Maps V st dom m2 = cod m1 & dom m3 = cod m2 holds
m3 * (m2 * m1) = (m3 * m2) * m1
proof end;

theorem Th14: :: ENS_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for m being Element of Maps V holds
( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )
proof end;

definition
let V be non empty set ;
let A, B be Element of V;
func Maps A,B -> set equals :: ENS_1:def 8
{ [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } ;
correctness
coherence
{ [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } is set
;
;
end;

:: deftheorem defines Maps ENS_1:def 8 :
for V being non empty set
for A, B being Element of V holds Maps A,B = { [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } ;

theorem Th15: :: ENS_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for A, B being Element of V
for f being Function of A,B st ( B = {} implies A = {} ) holds
[[A,B],f] in Maps A,B
proof end;

theorem Th16: :: ENS_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for A, B being Element of V
for m being Element of Maps V st m in Maps A,B holds
m = [[A,B],(m `2 )]
proof end;

theorem Th17: :: ENS_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for A, B being Element of V holds Maps A,B c= Maps V
proof end;

Lm4: for V being non empty set
for A, B being Element of V
for f being Function st [[A,B],f] in Maps A,B holds
( ( B = {} implies A = {} ) & f is Function of A,B )
proof end;

theorem :: ENS_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set holds Maps V = union { (Maps A,B) where A, B is Element of V : verum }
proof end;

theorem Th19: :: ENS_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for A, B being Element of V
for m being Element of Maps V holds
( m in Maps A,B iff ( dom m = A & cod m = B ) )
proof end;

theorem Th20: :: ENS_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for A, B being Element of V
for m being Element of Maps V st m in Maps A,B holds
m `2 in Funcs A,B
proof end;

Lm5: for V being non empty set
for W being non empty Subset of V
for A, B being Element of W
for A', B' being Element of V st A = A' & B = B' holds
Maps A,B = Maps A',B'
proof end;

definition
let V be non empty set ;
let m be Element of Maps V;
attr m is surjective means :: ENS_1:def 9
rng (m `2 ) = cod m;
end;

:: deftheorem defines surjective ENS_1:def 9 :
for V being non empty set
for m being Element of Maps V holds
( m is surjective iff rng (m `2 ) = cod m );

notation
let V be non empty set ;
let m be Element of Maps V;
synonym m is_a_surjection for surjective mm is_a_surjectionis_a_surjection ;
end;

definition
let V be non empty set ;
func fDom V -> Function of Maps V,V means :Def10: :: ENS_1:def 10
for m being Element of Maps V holds it . m = dom m;
existence
ex b1 being Function of Maps V,V st
for m being Element of Maps V holds b1 . m = dom m
proof end;
uniqueness
for b1, b2 being Function of Maps V,V st ( for m being Element of Maps V holds b1 . m = dom m ) & ( for m being Element of Maps V holds b2 . m = dom m ) holds
b1 = b2
proof end;
func fCod V -> Function of Maps V,V means :Def11: :: ENS_1:def 11
for m being Element of Maps V holds it . m = cod m;
existence
ex b1 being Function of Maps V,V st
for m being Element of Maps V holds b1 . m = cod m
proof end;
uniqueness
for b1, b2 being Function of Maps V,V st ( for m being Element of Maps V holds b1 . m = cod m ) & ( for m being Element of Maps V holds b2 . m = cod m ) holds
b1 = b2
proof end;
func fComp V -> PartFunc of [:(Maps V),(Maps V):], Maps V means :Def12: :: ENS_1:def 12
( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom it iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
it . [m2,m1] = m2 * m1 ) );
existence
ex b1 being PartFunc of [:(Maps V),(Maps V):], Maps V st
( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) )
proof end;
uniqueness
for b1, b2 being PartFunc of [:(Maps V),(Maps V):], Maps V st ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b2 . [m2,m1] = m2 * m1 ) holds
b1 = b2
proof end;
func fId V -> Function of V, Maps V means :Def13: :: ENS_1:def 13
for A being Element of V holds it . A = id$ A;
existence
ex b1 being Function of V, Maps V st
for A being Element of V holds b1 . A = id$ A
proof end;
uniqueness
for b1, b2 being Function of V, Maps V st ( for A being Element of V holds b1 . A = id$ A ) & ( for A being Element of V holds b2 . A = id$ A ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines fDom ENS_1:def 10 :
for V being non empty set
for b2 being Function of Maps V,V holds
( b2 = fDom V iff for m being Element of Maps V holds b2 . m = dom m );

:: deftheorem Def11 defines fCod ENS_1:def 11 :
for V being non empty set
for b2 being Function of Maps V,V holds
( b2 = fCod V iff for m being Element of Maps V holds b2 . m = cod m );

:: deftheorem Def12 defines fComp ENS_1:def 12 :
for V being non empty set
for b2 being PartFunc of [:(Maps V),(Maps V):], Maps V holds
( b2 = fComp V iff ( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b2 . [m2,m1] = m2 * m1 ) ) );

:: deftheorem Def13 defines fId ENS_1:def 13 :
for V being non empty set
for b2 being Function of V, Maps V holds
( b2 = fId V iff for A being Element of V holds b2 . A = id$ A );

definition
let V be non empty set ;
func Ens V -> CatStr equals :: ENS_1:def 14
CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #);
coherence
CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #) is CatStr
;
end;

:: deftheorem defines Ens ENS_1:def 14 :
for V being non empty set holds Ens V = CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #);

theorem Th21: :: ENS_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set holds CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #) is Category
proof end;

registration
let V be non empty set ;
cluster Ens V -> strict Category-like ;
coherence
( Ens V is strict & Ens V is Category-like )
by Th21;
end;

theorem :: ENS_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for A being Element of V holds A is Object of (Ens V) ;

definition
let V be non empty set ;
let A be Element of V;
func @ A -> Object of (Ens V) equals :: ENS_1:def 15
A;
coherence
A is Object of (Ens V)
;
end;

:: deftheorem defines @ ENS_1:def 15 :
for V being non empty set
for A being Element of V holds @ A = A;

theorem :: ENS_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for a being Object of (Ens V) holds a is Element of V ;

definition
let V be non empty set ;
let a be Object of (Ens V);
func @ a -> Element of V equals :: ENS_1:def 16
a;
coherence
a is Element of V
;
end;

:: deftheorem defines @ ENS_1:def 16 :
for V being non empty set
for a being Object of (Ens V) holds @ a = a;

theorem :: ENS_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for m being Element of Maps V holds m is Morphism of (Ens V) ;

definition
let V be non empty set ;
let m be Element of Maps V;
func @ m -> Morphism of (Ens V) equals :: ENS_1:def 17
m;
coherence
m is Morphism of (Ens V)
;
end;

:: deftheorem defines @ ENS_1:def 17 :
for V being non empty set
for m being Element of Maps V holds @ m = m;

theorem :: ENS_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for f being Morphism of (Ens V) holds f is Element of Maps V ;

definition
let V be non empty set ;
let f be Morphism of (Ens V);
func @ f -> Element of Maps V equals :: ENS_1:def 18
f;
coherence
f is Element of Maps V
;
end;

:: deftheorem defines @ ENS_1:def 18 :
for V being non empty set
for f being Morphism of (Ens V) holds @ f = f;

theorem Th26: :: ENS_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for f being Morphism of (Ens V) holds
( dom f = dom (@ f) & cod f = cod (@ f) ) by Def10, Def11;

theorem Th27: :: ENS_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for a, b being Object of (Ens V) holds Hom a,b = Maps (@ a),(@ b)
proof end;

Lm6: for V being non empty set
for a, b being Object of (Ens V) st Hom a,b <> {} holds
Funcs (@ a),(@ b) <> {}
proof end;

theorem Th28: :: ENS_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for g, f being Morphism of (Ens V) st dom g = cod f holds
g * f = (@ g) * (@ f)
proof end;

theorem Th29: :: ENS_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for a being Object of (Ens V) holds id a = id$ (@ a) by Def13;

theorem :: ENS_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for a being Object of (Ens V) st a = {} holds
a is initial
proof end;

theorem Th31: :: ENS_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for a being Object of (Ens V) st {} in V & a is initial holds
a = {}
proof end;

theorem :: ENS_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe
for a being Object of (Ens W) st a is initial holds
a = {}
proof end;

theorem :: ENS_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for a being Object of (Ens V) st ex x being set st a = {x} holds
a is terminal
proof end;

theorem Th34: :: ENS_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for a being Object of (Ens V) st V <> {{} } & a is terminal holds
ex x being set st a = {x}
proof end;

theorem :: ENS_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe
for a being Object of (Ens W) st a is terminal holds
ex x being set st a = {x}
proof end;

theorem :: ENS_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for f being Morphism of (Ens V) holds
( f is monic iff (@ f) `2 is one-to-one )
proof end;

theorem Th37: :: ENS_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for f being Morphism of (Ens V) st f is epi & ex A being Element of V ex x1, x2 being set st
( x1 in A & x2 in A & x1 <> x2 ) holds
@ f is surjective
proof end;

theorem :: ENS_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for f being Morphism of (Ens V) st @ f is surjective holds
f is epi
proof end;

theorem :: ENS_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe
for f being Morphism of (Ens W) st f is epi holds
@ f is surjective
proof end;

theorem :: ENS_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for W being non empty Subset of V holds Ens W is_full_subcategory_of Ens V
proof end;

definition
let C be Category;
func Hom C -> set equals :: ENS_1:def 19
{ (Hom a,b) where a, b is Object of C : verum } ;
coherence
{ (Hom a,b) where a, b is Object of C : verum } is set
;
end;

:: deftheorem defines Hom ENS_1:def 19 :
for C being Category holds Hom C = { (Hom a,b) where a, b is Object of C : verum } ;

registration
let C be Category;
cluster Hom C -> non empty ;
coherence
not Hom C is empty
proof end;
end;

theorem :: ENS_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, b being Object of C holds Hom a,b in Hom C ;

theorem :: ENS_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of C
for f being Morphism of C holds
( ( Hom a,(cod f) = {} implies Hom a,(dom f) = {} ) & ( Hom (dom f),a = {} implies Hom (cod f),a = {} ) )
proof end;

definition
let C be Category;
let a be Object of C;
let f be Morphism of C;
func hom a,f -> Function of Hom a,(dom f), Hom a,(cod f) means :Def20: :: ENS_1:def 20
for g being Morphism of C st g in Hom a,(dom f) holds
it . g = f * g;
existence
ex b1 being Function of Hom a,(dom f), Hom a,(cod f) st
for g being Morphism of C st g in Hom a,(dom f) holds
b1 . g = f * g
proof end;
uniqueness
for b1, b2 being Function of Hom a,(dom f), Hom a,(cod f) st ( for g being Morphism of C st g in Hom a,(dom f) holds
b1 . g = f * g ) & ( for g being Morphism of C st g in Hom a,(dom f) holds
b2 . g = f * g ) holds
b1 = b2
proof end;
func hom f,a -> Function of Hom (cod f),a, Hom (dom f),a means :Def21: :: ENS_1:def 21
for g being Morphism of C st g in Hom (cod f),a holds
it . g = g * f;
existence
ex b1 being Function of Hom (cod f),a, Hom (dom f),a st
for g being Morphism of C st g in Hom (cod f),a holds
b1 . g = g * f
proof end;
uniqueness
for b1, b2 being Function of Hom (cod f),a, Hom (dom f),a st ( for g being Morphism of C st g in Hom (cod f),a holds
b1 . g = g * f ) & ( for g being Morphism of C st g in Hom (cod f),a holds
b2 . g = g * f ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines hom ENS_1:def 20 :
for C being Category
for a being Object of C
for f being Morphism of C
for b4 being Function of Hom a,(dom f), Hom a,(cod f) holds
( b4 = hom a,f iff for g being Morphism of C st g in Hom a,(dom f) holds
b4 . g = f * g );

:: deftheorem Def21 defines hom ENS_1:def 21 :
for C being Category
for a being Object of C
for f being Morphism of C
for b4 being Function of Hom (cod f),a, Hom (dom f),a holds
( b4 = hom f,a iff for g being Morphism of C st g in Hom (cod f),a holds
b4 . g = g * f );

theorem Th43: :: ENS_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, c being Object of C holds hom a,(id c) = id (Hom a,c)
proof end;

theorem Th44: :: ENS_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for c, a being Object of C holds hom (id c),a = id (Hom c,a)
proof end;

theorem Th45: :: ENS_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of C
for g, f being Morphism of C st dom g = cod f holds
hom a,(g * f) = (hom a,g) * (hom a,f)
proof end;

theorem Th46: :: ENS_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of C
for g, f being Morphism of C st dom g = cod f holds
hom (g * f),a = (hom f,a) * (hom g,a)
proof end;

theorem Th47: :: ENS_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of C
for f being Morphism of C holds [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)] is Element of Maps (Hom C)
proof end;

theorem Th48: :: ENS_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of C
for f being Morphism of C holds [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] is Element of Maps (Hom C)
proof end;

definition
let C be Category;
let a be Object of C;
func hom?- a -> Function of the Morphisms of C, Maps (Hom C) means :Def22: :: ENS_1:def 22
for f being Morphism of C holds it . f = [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)];
existence
ex b1 being Function of the Morphisms of C, Maps (Hom C) st
for f being Morphism of C holds b1 . f = [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)]
proof end;
uniqueness
for b1, b2 being Function of the Morphisms of C, Maps (Hom C) st ( for f being Morphism of C holds b1 . f = [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)] ) & ( for f being Morphism of C holds b2 . f = [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)] ) holds
b1 = b2
proof end;
func hom-? a -> Function of the Morphisms of C, Maps (Hom C) means :Def23: :: ENS_1:def 23
for f being Morphism of C holds it . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)];
existence
ex b1 being Function of the Morphisms of C, Maps (Hom C) st
for f being Morphism of C holds b1 . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)]
proof end;
uniqueness
for b1, b2 being Function of the Morphisms of C, Maps (Hom C) st ( for f being Morphism of C holds b1 . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] ) & ( for f being Morphism of C holds b2 . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines hom?- ENS_1:def 22 :
for C being Category
for a being Object of C
for b3 being Function of the Morphisms of C, Maps (Hom C) holds
( b3 = hom?- a iff for f being Morphism of C holds b3 . f = [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)] );

:: deftheorem Def23 defines hom-? ENS_1:def 23 :
for C being Category
for a being Object of C
for b3 being Function of the Morphisms of C, Maps (Hom C) holds
( b3 = hom-? a iff for f being Morphism of C holds b3 . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] );

Lm7: for V being non empty set
for C being Category
for T being Function of the Morphisms of C, Maps (Hom C) st Hom C c= V holds
T is Function of the Morphisms of C,the Morphisms of (Ens V)
proof end;

Lm8: for V being non empty set
for C being Category
for a, c being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom a,c holds
(hom?- a) . (id c) = id d
proof end;

Lm9: for V being non empty set
for C being Category
for c, a being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom c,a holds
(hom-? a) . (id c) = id d
proof end;

theorem Th49: :: ENS_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
hom?- a is Functor of C, Ens V
proof end;

theorem Th50: :: ENS_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
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
proof end;

theorem Th51: :: ENS_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f, f' being Morphism of C st Hom (dom f),(cod f') = {} holds
Hom (cod f),(dom f') = {}
proof end;

definition
let C be Category;
let f, g be Morphism of C;
func hom f,g -> Function of Hom (cod f),(dom g), Hom (dom f),(cod g) means :Def24: :: ENS_1:def 24
for h being Morphism of C st h in Hom (cod f),(dom g) holds
it . h = (g * h) * f;
existence
ex b1 being Function of Hom (cod f),(dom g), Hom (dom f),(cod g) st
for h being Morphism of C st h in Hom (cod f),(dom g) holds
b1 . h = (g * h) * f
proof end;
uniqueness
for b1, b2 being Function of Hom (cod f),(dom g), Hom (dom f),(cod g) st ( for h being Morphism of C st h in Hom (cod f),(dom g) holds
b1 . h = (g * h) * f ) & ( for h being Morphism of C st h in Hom (cod f),(dom g) holds
b2 . h = (g * h) * f ) holds
b1 = b2
proof end;
end;

:: deftheorem Def24 defines hom ENS_1:def 24 :
for C being Category
for f, g being Morphism of C
for b4 being Function of Hom (cod f),(dom g), Hom (dom f),(cod g) holds
( b4 = hom f,g iff for h being Morphism of C st h in Hom (cod f),(dom g) holds
b4 . h = (g * h) * f );

theorem Th52: :: ENS_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f, g being Morphism of C holds [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)] is Element of Maps (Hom C)
proof end;

theorem Th53: :: ENS_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of C
for f being Morphism of C holds
( hom (id a),f = hom a,f & hom f,(id a) = hom f,a )
proof end;

theorem Th54: :: ENS_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a, b being Object of C holds hom (id a),(id b) = id (Hom a,b)
proof end;

theorem :: ENS_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for f, g being Morphism of C holds hom f,g = (hom (dom f),g) * (hom f,(dom g))
proof end;

theorem Th56: :: ENS_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for g, f, g', f' being Morphism of C st cod g = dom f & dom g' = cod f' holds
hom (f * g),(g' * f') = (hom g,g') * (hom f,f')
proof end;

definition
let C be Category;
func hom?? C -> Function of the Morphisms of [:C,C:], Maps (Hom C) means :Def25: :: ENS_1:def 25
for f, g being Morphism of C holds it . [f,g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)];
existence
ex b1 being Function of the Morphisms of [:C,C:], Maps (Hom C) st
for f, g being Morphism of C holds b1 . [f,g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)]
proof end;
uniqueness
for b1, b2 being Function of the Morphisms of [:C,C:], Maps (Hom C) st ( for f, g being Morphism of C holds b1 . [f,g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)] ) & ( for f, g being Morphism of C holds b2 . [f,g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def25 defines hom?? ENS_1:def 25 :
for C being Category
for b2 being Function of the Morphisms of [:C,C:], Maps (Hom C) holds
( b2 = hom?? C iff for f, g being Morphism of C holds b2 . [f,g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)] );

theorem Th57: :: ENS_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Category
for a being Object of C holds
( hom?- a = (curry (hom?? C)) . (id a) & hom-? a = (curry' (hom?? C)) . (id a) )
proof end;

Lm10: for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom a,b holds
(hom?? C) . [(id a),(id b)] = id d
proof end;

theorem Th58: :: ENS_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for C being Category st Hom C c= V holds
hom?? C is Functor of [:(C opp ),C:], Ens V
proof end;

definition
let V be non empty set ;
let C be Category;
let a be Object of C;
assume A1: Hom C c= V ;
func hom?- V,a -> Functor of C, Ens V equals :Def26: :: ENS_1:def 26
hom?- a;
coherence
hom?- a is Functor of C, Ens V
by A1, Th49;
func hom-? V,a -> Contravariant_Functor of C, Ens V equals :Def27: :: ENS_1:def 27
hom-? a;
coherence
hom-? a is Contravariant_Functor of C, Ens V
by A1, Th50;
end;

:: deftheorem Def26 defines hom?- ENS_1:def 26 :
for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
hom?- V,a = hom?- a;

:: deftheorem Def27 defines hom-? ENS_1:def 27 :
for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
hom-? V,a = hom-? a;

definition
let V be non empty set ;
let C be Category;
assume A1: Hom C c= V ;
func hom?? V,C -> Functor of [:(C opp ),C:], Ens V equals :Def28: :: ENS_1:def 28
hom?? C;
coherence
hom?? C is Functor of [:(C opp ),C:], Ens V
by A1, Th58;
end;

:: deftheorem Def28 defines hom?? ENS_1:def 28 :
for V being non empty set
for C being Category st Hom C c= V holds
hom?? V,C = hom?? C;

theorem :: ENS_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for C being Category
for a being Object of C
for f being Morphism of C st Hom C c= V holds
(hom?- V,a) . f = [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)]
proof end;

theorem :: ENS_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
(Obj (hom?- V,a)) . b = Hom a,b
proof end;

theorem :: ENS_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for C being Category
for a being Object of C
for f being Morphism of C st Hom C c= V holds
(hom-? V,a) . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)]
proof end;

theorem :: ENS_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
(Obj (hom-? V,a)) . b = Hom b,a
proof end;

theorem :: ENS_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for C being Category
for f, g being Morphism of C st Hom C c= V holds
(hom?? V,C) . [(f opp ),g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)]
proof end;

theorem :: ENS_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
(Obj (hom?? V,C)) . [(a opp ),b] = Hom a,b
proof end;

theorem :: ENS_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
(hom?? V,C) ?- (a opp ) = hom?- V,a
proof end;

theorem :: ENS_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
(hom?? V,C) -? a = hom-? V,a
proof end;