:: ENS_1 semantic presentation

begin


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 ->  functional non empty ;
coherence
 ( Funcs V is functional & not Funcs V is empty )
proof
set F =  {  (Funcs (A,B)) where A, B is Element of V : verum  }  ;
set A = the Element of V;
 ( id the Element of V in Funcs ( the Element of V, the Element of V) & Funcs ( the Element of V, the Element of V) in  {  (Funcs (A,B)) where A, B is Element of V : verum  }  ) by FUNCT_2:9;
then reconsider UF = union  {  (Funcs (A,B)) where A, B is Element of V : verum  }  as non empty set by TARSKI:def_4;
now__::_thesis:_for_f_being_set_st_f_in_UF_holds_
f_is_Function
let f be set ; ::_thesis: ( f in UF implies f is Function )
assume  f in UF ; ::_thesis: f is Function
then consider C being set  such that
A1: f in C and
A2: C in  {  (Funcs (A,B)) where A, B is Element of V : verum  }  by TARSKI:def_4;
 ex A, B being Element of V st C = Funcs (A,B) by A2;
hence  f is Function by A1; ::_thesis: verum
end;
hence  ( Funcs V is functional & not Funcs V is empty ) by FUNCT_1:def_13; ::_thesis: verum
end;
end;

theorem Th1: :: ENS_1:1
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
let V be non empty set ; ::_thesis: 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 ) )
let f be set ; ::_thesis: ( f in Funcs V iff ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B ) )
set F =  {  (Funcs (A,B)) where A, B is Element of V : verum  }  ;
thus  ( f in Funcs V implies ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B ) ) ::_thesis: ( ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B ) implies f in Funcs V )
proof
assume  f in Funcs V ; ::_thesis: ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B )
then consider C being set  such that
A1: f in C and
A2: C in  {  (Funcs (A,B)) where A, B is Element of V : verum  }  by TARSKI:def_4;
consider A, B being Element of V such that
A3: C = Funcs (A,B) by A2;
take  A ; ::_thesis: ex B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B )
take  B ; ::_thesis: ( ( B = {} implies A = {} ) & f is Function of A,B )
thus  ( ( B = {} implies A = {} ) & f is Function of A,B ) by A1, A3, FUNCT_2:66; ::_thesis: verum
end;
given A, B being Element of V such that A4: ( ( B = {} implies A = {} ) & f is Function of A,B ) ; ::_thesis: f in Funcs V
A5: Funcs (A,B) in  {  (Funcs (A,B)) where A, B is Element of V : verum  }  ;
 f in Funcs (A,B) by A4, FUNCT_2:8;
hence  f in Funcs V by A5, TARSKI:def_4; ::_thesis: verum
end;

theorem :: ENS_1:2
for V being non empty set
for A, B being Element of V holds Funcs (A,B) c= Funcs V
proof
let V be non empty set ; ::_thesis: for A, B being Element of V holds Funcs (A,B) c= Funcs V
let A, B be Element of V; ::_thesis: Funcs (A,B) c= Funcs V
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (A,B) or x in Funcs V )
assume A1: x in Funcs (A,B) ; ::_thesis: x in Funcs V
then A2: x is Function of A,B by FUNCT_2:66;
 ( B = {} implies A = {} ) by A1;
hence  x in Funcs V by A2, Th1; ::_thesis: verum
end;

theorem Th3: :: ENS_1:3
for V being non empty set
for W being non empty Subset of V holds Funcs W c= Funcs V
proof
let V be non empty set ; ::_thesis: for W being non empty Subset of V holds Funcs W c= Funcs V
let W be non empty Subset of V; ::_thesis: Funcs W c= Funcs V
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in Funcs W or f in Funcs V )
assume  f in Funcs W ; ::_thesis: f in Funcs V
then  ex A, B being Element of W st
( ( B = {} implies A = {} ) & f is Function of A,B ) by Th1;
hence  f in Funcs V by Th1; ::_thesis: verum
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
set FV =  {  [[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 )  }  ;
set A = the Element of V;
now__::_thesis:_ex_m_being_Element_of_[:[:V,V:],(bool_[:_the_Element_of_V,_the_Element_of_V:]):]_st_m_in__{__[[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_)__}_
set f = id the Element of V;
take m = [[ the Element of V, the Element of V],(id the Element of V)]; ::_thesis: m in  {  [[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 )  }
A1: ( the Element of V = {} implies the Element of V = {} ) ;
 id the Element of V in Funcs V by Th1;
hence  m in  {  [[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 )  }  by A1; ::_thesis: verum
end;
hence  not Maps V is empty ; ::_thesis: verum
end;
end;


theorem Th4: :: ENS_1:4
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
let V be non empty set ; ::_thesis: 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 )
let m be Element of Maps V; ::_thesis: 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 )
 m in  {  [[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 )  }  ;
then  ex A, B being Element of V ex f being Element of Funcs V st
( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B ) ;
hence  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 ) ; ::_thesis: verum
end;

theorem Th5: :: ENS_1:5
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
let V be non empty set ; ::_thesis: 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
let A, B be Element of V; ::_thesis: for f being Function of A,B st ( B = {} implies A = {} ) holds
[[A,B],f] in Maps V
let f be Function of A,B; ::_thesis: ( ( B = {} implies A = {} ) implies [[A,B],f] in Maps V )
assume A1: ( B = {} implies A = {} ) ; ::_thesis: [[A,B],f] in Maps V
then  f in Funcs V by Th1;
hence  [[A,B],f] in Maps V by A1; ::_thesis: verum
end;

theorem :: ENS_1:6
for V being non empty set holds Maps V c= [:[:V,V:],(Funcs V):]
proof
let V be non empty set ; ::_thesis: Maps V c= [:[:V,V:],(Funcs V):]
let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in Maps V or m in [:[:V,V:],(Funcs V):] )
assume  m in Maps V ; ::_thesis: m in [:[:V,V:],(Funcs V):]
then  ex A, B being Element of V ex f being Element of Funcs V st
( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B ) ;
hence  m in [:[:V,V:],(Funcs V):] ; ::_thesis: verum
end;

theorem Th7: :: ENS_1:7
for V being non empty set
for W being non empty Subset of V holds Maps W c= Maps V
proof
let V be non empty set ; ::_thesis: for W being non empty Subset of V holds Maps W c= Maps V
let W be non empty Subset of V; ::_thesis: Maps W c= Maps V
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Maps W or x in Maps V )
assume  x in Maps W ; ::_thesis: x in Maps V
then consider A, B being Element of W, f being Element of Funcs W such that
A1: ( x = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B ) ;
 ( Funcs W c= Funcs V & f in Funcs W ) by Th3;
hence  x in Maps V by A1; ::_thesis: verum
end;

Lm1:  for x1, y1, x2, y2, x3, y3 being set st [[x1,x2],x3] = [[y1,y2],y3] holds
( x1 = y1 & x2 = y2 )
proof
let x1, y1, x2, y2, x3, y3 be set ; ::_thesis: ( [[x1,x2],x3] = [[y1,y2],y3] implies ( x1 = y1 & x2 = y2 ) )
assume  [[x1,x2],x3] = [[y1,y2],y3] ; ::_thesis: ( x1 = y1 & x2 = y2 )
then  [x1,x2] = [y1,y2] by XTUPLE_0:1;
hence  ( x1 = y1 & x2 = y2 ) by XTUPLE_0:1; ::_thesis: verum
end;

registration
let V be non empty set ;
let m be Element of Maps V;
clusterm `2  ->  Relation-like Function-like ;
coherence
 ( m `2 is Function-like & m `2 is Relation-like )
proof
 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 ) by Th4;
hence  ( m `2 is Function-like & m `2 is Relation-like ) by MCART_1:7; ::_thesis: verum
end;
end;

definition
let V be non empty set ;
let m be Element of Maps V;
func dom m ->  Element of V equals :: ENS_1:def 3
(m `1) `1 ;
coherence
 (m `1) `1 is Element of V
proof
consider f being Element of Funcs V, A, B being Element of V such that
A1: m = [[A,B],f] and
 ( B = {} implies A = {} ) and
 f is Function of A,B by Th4;
 [A,B] = m `1 by A1, MCART_1:7;
hence  (m `1) `1 is Element of V by MCART_1:7; ::_thesis: verum
end;
func cod m ->  Element of V equals :: ENS_1:def 4
(m `1) `2 ;
coherence
 (m `1) `2 is Element of V
proof
consider f being Element of Funcs V, A, B being Element of V such that
A2: m = [[A,B],f] and
 ( B = {} implies A = {} ) and
 f is Function of A,B by Th4;
 [A,B] = m `1 by A2, MCART_1:7;
hence  (m `1) `2 is Element of V by MCART_1:7; ::_thesis: verum
end;
end;

:: deftheorem  defines dom ENS_1:def_3_:_
 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_4_:_
 for V being non empty set
for m being Element of Maps V holds cod m = (m `1) `2 ;

theorem Th8: :: ENS_1:8
for V being non empty set
for m being Element of Maps V holds m = [[(dom m),(cod m)],(m `2)]
proof
let V be non empty set ; ::_thesis: for m being Element of Maps V holds m = [[(dom m),(cod m)],(m `2)]
let m be Element of Maps V; ::_thesis: m = [[(dom m),(cod m)],(m `2)]
consider f being Element of Funcs V, A, B being Element of V such that
A1: ( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B ) by Th4;
 m `1 = [A,B] by A1, MCART_1:7;
then  m `1 = [(dom m),(cod m)] by MCART_1:8;
hence  m = [[(dom m),(cod m)],(m `2)] by A1, MCART_1:8; ::_thesis: verum
end;

Lm2:  for V being non empty set
for m, m9 being Element of Maps V st m `2 = m9 `2 & dom m = dom m9 & cod m = cod m9 holds
m = m9
proof
let V be non empty set ; ::_thesis: for m, m9 being Element of Maps V st m `2 = m9 `2 & dom m = dom m9 & cod m = cod m9 holds
m = m9
let m, m9 be Element of Maps V; ::_thesis: ( m `2 = m9 `2 & dom m = dom m9 & cod m = cod m9 implies m = m9 )
 m = [[(dom m),(cod m)],(m `2)] by Th8;
hence  ( m `2 = m9 `2 & dom m = dom m9 & cod m = cod m9 implies m = m9 ) by Th8; ::_thesis: verum
end;

theorem Th9: :: ENS_1:9
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
let V be non empty set ; ::_thesis: for m being Element of Maps V holds
( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) )
let m be Element of Maps V; ::_thesis: ( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) )
consider f being Element of Funcs V, A, B being Element of V such that
A1: m = [[A,B],f] and
A2: ( ( B = {} implies A = {} ) & f is Function of A,B ) by Th4;
A3: m = [[(dom m),(cod m)],(m `2)] by Th8;
then  ( f = m `2 & A = dom m ) by A1, Lm1, XTUPLE_0:1;
hence  ( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) ) by A1, A2, A3, Lm1; ::_thesis: verum
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
let V be non empty set ; ::_thesis: for m being Element of Maps V holds
( dom (m `2) = dom m & rng (m `2) c= cod m )
let m be Element of Maps V; ::_thesis: ( dom (m `2) = dom m & rng (m `2) c= cod m )
A1: m `2 is Function of (dom m),(cod m) by Th9;
 ( cod m <> {} or dom m = {} ) by Th9;
hence  ( dom (m `2) = dom m & rng (m `2) c= cod m ) by A1, FUNCT_2:def_1, RELAT_1:def_19; ::_thesis: verum
end;

theorem Th10: :: ENS_1:10
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
let V be non empty set ; ::_thesis: 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 )
let f be Function; ::_thesis: for A, B being set st [[A,B],f] in Maps V holds
( ( B = {} implies A = {} ) & f is Function of A,B )
let A, B be set ; ::_thesis: ( [[A,B],f] in Maps V implies ( ( B = {} implies A = {} ) & f is Function of A,B ) )
assume  [[A,B],f] in Maps V ; ::_thesis: ( ( B = {} implies A = {} ) & f is Function of A,B )
then consider f9 being Element of Funcs V, A9, B9 being Element of V such that
A1: [[A,B],f] = [[A9,B9],f9] and
A2: ( ( B9 = {} implies A9 = {} ) & f9 is Function of A9,B9 ) by Th4;
 ( f = f9 & A = A9 ) by A1, Lm1, XTUPLE_0:1;
hence  ( ( B = {} implies A = {} ) & f is Function of A,B ) by A1, A2, Lm1; ::_thesis: verum
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 5
[[A,A],(id A)];
coherence
 [[A,A],(id A)] is Element of Maps V by Th5;
end;

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

theorem Th11: :: ENS_1:11
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
let V be non empty set ; ::_thesis: for A being Element of V holds
( (id$ A) `2 = id A & dom (id$ A) = A & cod (id$ A) = A )
let A be Element of V; ::_thesis: ( (id$ A) `2 = id A & dom (id$ A) = A & cod (id$ A) = A )
 [[(dom (id$ A)),(cod (id$ A))],((id$ A) `2)] = [[A,A],(id A)] by Th8;
hence  ( (id$ A) `2 = id A & dom (id$ A) = A & cod (id$ A) = A ) by Lm1, XTUPLE_0:1; ::_thesis: verum
end;

definition
let V be non empty set ;
let m1, m2 be Element of Maps V;
assume A1: cod m1 = dom m2 ;
funcm2 * m1 ->  Element of Maps V equals :Def6: :: ENS_1:def 6
[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];
coherence
 [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of Maps V
proof
A2: ( cod m2 <> {} or dom m2 = {} ) by Th9;
A3: ( cod m1 <> {} or dom m1 = {} ) by Th9;
 ( m1 `2 is Function of (dom m1),(cod m1) & m2 `2 is Function of (dom m2),(cod m2) ) by Th9;
then  (m2 `2) * (m1 `2) is Function of (dom m1),(cod m2) by A1, A3, FUNCT_2:13;
hence  [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of Maps V by A1, A3, A2, Th5; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines * ENS_1:def_6_:_
 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
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
let V be non empty set ; ::_thesis: 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 )
let m2, m1 be Element of Maps V; ::_thesis: ( dom m2 = cod m1 implies ( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 ) )
assume  dom m2 = cod m1 ; ::_thesis: ( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 )
then [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] = m2 * m1 by Def6
.= [[(dom (m2 * m1)),(cod (m2 * m1))],((m2 * m1) `2)] by Th8 ;
hence  ( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 ) by Lm1, XTUPLE_0:1; ::_thesis: verum
end;

theorem Th13: :: ENS_1:13
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
let V be non empty set ; ::_thesis: 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
let m2, m1, m3 be Element of Maps V; ::_thesis: ( dom m2 = cod m1 & dom m3 = cod m2 implies m3 * (m2 * m1) = (m3 * m2) * m1 )
assume that
A1: dom m2 = cod m1 and
A2: dom m3 = cod m2 ; ::_thesis: m3 * (m2 * m1) = (m3 * m2) * m1
A3: cod (m2 * m1) = cod m2 by A1, Th12;
 (m2 * m1) `2 = (m2 `2) * (m1 `2) by A1, Th12;
then A4: (m3 * (m2 * m1)) `2 = (m3 `2) * ((m2 `2) * (m1 `2)) by A2, A3, Th12;
A5: dom (m3 * m2) = dom m2 by A2, Th12;
then A6: dom ((m3 * m2) * m1) = dom m1 by A1, Th12;
 dom (m2 * m1) = dom m1 by A1, Th12;
then A7: dom (m3 * (m2 * m1)) = dom m1 by A2, A3, Th12;
 cod (m3 * m2) = cod m3 by A2, Th12;
then A8: cod ((m3 * m2) * m1) = cod m3 by A1, A5, Th12;
 (m3 * m2) `2 = (m3 `2) * (m2 `2) by A2, Th12;
then A9: ((m3 * m2) * m1) `2 = ((m3 `2) * (m2 `2)) * (m1 `2) by A1, A5, Th12;
 cod (m3 * (m2 * m1)) = cod m3 by A2, A3, Th12;
hence  m3 * (m2 * m1) = (m3 * m2) * m1 by A4, A7, A9, A6, A8, Lm2, RELAT_1:36; ::_thesis: verum
end;

theorem Th14: :: ENS_1:14
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
let V be non empty set ; ::_thesis: for m being Element of Maps V holds
( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )
let m be Element of Maps V; ::_thesis: ( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )
set i1 = id$ (dom m);
set i2 = id$ (cod m);
A1: ( (id$ (dom m)) `2 = id (dom m) & dom (id$ (dom m)) = dom m ) by Th11;
A2: m `2 is Function of (dom m),(cod m) by Th9;
then A3: rng (m `2) c= cod m by RELAT_1:def_19;
 ( cod m <> {} or dom m = {} ) by Th9;
then A4: dom (m `2) = dom m by A2, FUNCT_2:def_1;
A5: cod (id$ (dom m)) = dom m by Th11;
then A6: cod (m * (id$ (dom m))) = cod m by Th12;
 ( (m * (id$ (dom m))) `2 = (m `2) * ((id$ (dom m)) `2) & dom (m * (id$ (dom m))) = dom (id$ (dom m)) ) by A5, Th12;
hence  m * (id$ (dom m)) = m by A4, A1, A6, Lm2, RELAT_1:52; ::_thesis: (id$ (cod m)) * m = m
A7: ( (id$ (cod m)) `2 = id (cod m) & cod (id$ (cod m)) = cod m ) by Th11;
A8: dom (id$ (cod m)) = cod m by Th11;
then A9: cod ((id$ (cod m)) * m) = cod (id$ (cod m)) by Th12;
 ( ((id$ (cod m)) * m) `2 = ((id$ (cod m)) `2) * (m `2) & dom ((id$ (cod m)) * m) = dom m ) by A8, Th12;
hence  (id$ (cod m)) * m = m by A3, A7, A9, Lm2, RELAT_1:53; ::_thesis: verum
end;

definition
let V be non empty set ;
let A, B be Element of V;
func Maps (A,B) ->  set  equals :: ENS_1:def 7
 {  [[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_7_:_
 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
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
let V be non empty set ; ::_thesis: 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)
let A, B be Element of V; ::_thesis: for f being Function of A,B st ( B = {} implies A = {} ) holds
[[A,B],f] in Maps (A,B)
let f be Function of A,B; ::_thesis: ( ( B = {} implies A = {} ) implies [[A,B],f] in Maps (A,B) )
assume  ( B = {} implies A = {} ) ; ::_thesis: [[A,B],f] in Maps (A,B)
then  ( f in Funcs V & [[A,B],f] in Maps V ) by Th1, Th5;
hence  [[A,B],f] in Maps (A,B) ; ::_thesis: verum
end;

theorem Th16: :: ENS_1:16
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
let V be non empty set ; ::_thesis: 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)]
let A, B be Element of V; ::_thesis: for m being Element of Maps V st m in Maps (A,B) holds
m = [[A,B],(m `2)]
let m be Element of Maps V; ::_thesis: ( m in Maps (A,B) implies m = [[A,B],(m `2)] )
assume  m in Maps (A,B) ; ::_thesis: m = [[A,B],(m `2)]
then A1: ex f being Element of Funcs V st
( m = [[A,B],f] & [[A,B],f] in Maps V ) ;
 m = [[(dom m),(cod m)],(m `2)] by Th8;
hence  m = [[A,B],(m `2)] by A1, XTUPLE_0:1; ::_thesis: verum
end;

theorem Th17: :: ENS_1:17
for V being non empty set
for A, B being Element of V holds Maps (A,B) c= Maps V
proof
let V be non empty set ; ::_thesis: for A, B being Element of V holds Maps (A,B) c= Maps V
let A, B be Element of V; ::_thesis: Maps (A,B) c= Maps V
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Maps (A,B) or z in Maps V )
assume  z in Maps (A,B) ; ::_thesis: z in Maps V
then  ex f being Element of Funcs V st
( z = [[A,B],f] & [[A,B],f] in Maps V ) ;
hence  z in Maps V ; ::_thesis: verum
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
let V be non empty set ; ::_thesis: 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 )
let A, B be Element of V; ::_thesis: for f being Function st [[A,B],f] in Maps (A,B) holds
( ( B = {} implies A = {} ) & f is Function of A,B )
A1: Maps (A,B) c= Maps V by Th17;
let f be Function; ::_thesis: ( [[A,B],f] in Maps (A,B) implies ( ( B = {} implies A = {} ) & f is Function of A,B ) )
assume  [[A,B],f] in Maps (A,B) ; ::_thesis: ( ( B = {} implies A = {} ) & f is Function of A,B )
hence  ( ( B = {} implies A = {} ) & f is Function of A,B ) by A1, Th10; ::_thesis: verum
end;

theorem :: ENS_1:18
for V being non empty set holds Maps V = union  {  (Maps (A,B)) where A, B is Element of V : verum  }
proof
let V be non empty set ; ::_thesis: Maps V = union  {  (Maps (A,B)) where A, B is Element of V : verum  }
set M =  {  (Maps (A,B)) where A, B is Element of V : verum  }  ;
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_Maps_V_implies_z_in_union__{__(Maps_(A,B))_where_A,_B_is_Element_of_V_:_verum__}__)_&_(_z_in_union__{__(Maps_(A,B))_where_A,_B_is_Element_of_V_:_verum__}__implies_z_in_Maps_V_)_)
let z be set ; ::_thesis: ( ( z in Maps V implies z in union  {  (Maps (A,B)) where A, B is Element of V : verum  }  ) & ( z in union  {  (Maps (A,B)) where A, B is Element of V : verum  }  implies z in Maps V ) )
thus  ( z in Maps V implies z in union  {  (Maps (A,B)) where A, B is Element of V : verum  }  ) ::_thesis: ( z in union  {  (Maps (A,B)) where A, B is Element of V : verum  }  implies z in Maps V )
proof
assume  z in Maps V ; ::_thesis: z in union  {  (Maps (A,B)) where A, B is Element of V : verum  }
then consider f being Element of Funcs V, A, B being Element of V such that
A1: ( z = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B ) by Th4;
A2: Maps (A,B) in  {  (Maps (A,B)) where A, B is Element of V : verum  }  ;
 z in Maps (A,B) by A1, Th15;
hence  z in union  {  (Maps (A,B)) where A, B is Element of V : verum  }  by A2, TARSKI:def_4; ::_thesis: verum
end;
assume  z in union  {  (Maps (A,B)) where A, B is Element of V : verum  }  ; ::_thesis: z in Maps V
then consider C being set  such that
A3: z in C and
A4: C in  {  (Maps (A,B)) where A, B is Element of V : verum  }  by TARSKI:def_4;
consider A, B being Element of V such that
A5: C = Maps (A,B) by A4;
 ex f being Element of Funcs V st
( z = [[A,B],f] & [[A,B],f] in Maps V ) by A3, A5;
hence  z in Maps V ; ::_thesis: verum
end;
hence  Maps V = union  {  (Maps (A,B)) where A, B is Element of V : verum  }  by TARSKI:1; ::_thesis: verum
end;

theorem Th19: :: ENS_1:19
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
let V be non empty set ; ::_thesis: 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 ) )
let A, B be Element of V; ::_thesis: for m being Element of Maps V holds
( m in Maps (A,B) iff ( dom m = A & cod m = B ) )
let m be Element of Maps V; ::_thesis: ( m in Maps (A,B) iff ( dom m = A & cod m = B ) )
A1: m `2 is Function of (dom m),(cod m) by Th9;
thus  ( m in Maps (A,B) implies ( dom m = A & cod m = B ) ) ::_thesis: ( dom m = A & cod m = B implies m in Maps (A,B) )
proof
assume  m in Maps (A,B) ; ::_thesis: ( dom m = A & cod m = B )
then A2: m = [[A,B],(m `2)] by Th16;
 m = [[(dom m),(cod m)],(m `2)] by Th8;
hence  ( dom m = A & cod m = B ) by A2, Lm1; ::_thesis: verum
end;
 ( cod m <> {} or dom m = {} ) by Th9;
then  [[(dom m),(cod m)],(m `2)] in Maps ((dom m),(cod m)) by A1, Th15;
hence  ( dom m = A & cod m = B implies m in Maps (A,B) ) by Th8; ::_thesis: verum
end;

theorem Th20: :: ENS_1:20
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
let V be non empty set ; ::_thesis: 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)
let A, B be Element of V; ::_thesis: for m being Element of Maps V st m in Maps (A,B) holds
m `2 in Funcs (A,B)
let m be Element of Maps V; ::_thesis: ( m in Maps (A,B) implies m `2 in Funcs (A,B) )
assume A1: m in Maps (A,B) ; ::_thesis: m `2 in Funcs (A,B)
then A2: m = [[A,B],(m `2)] by Th16;
then A3: m `2 is Function of A,B by A1, Lm4;
 ( B = {} implies A = {} ) by A1, A2, Lm4;
hence  m `2 in Funcs (A,B) by A3, FUNCT_2:8; ::_thesis: verum
end;

Lm5:  for V being non empty set
for W being non empty Subset of V
for A, B being Element of W
for A9, B9 being Element of V st A = A9 & B = B9 holds
Maps (A,B) = Maps (A9,B9)
proof
let V be non empty set ; ::_thesis: for W being non empty Subset of V
for A, B being Element of W
for A9, B9 being Element of V st A = A9 & B = B9 holds
Maps (A,B) = Maps (A9,B9)
let W be non empty Subset of V; ::_thesis: for A, B being Element of W
for A9, B9 being Element of V st A = A9 & B = B9 holds
Maps (A,B) = Maps (A9,B9)
let A, B be Element of W; ::_thesis: for A9, B9 being Element of V st A = A9 & B = B9 holds
Maps (A,B) = Maps (A9,B9)
let A9, B9 be Element of V; ::_thesis: ( A = A9 & B = B9 implies Maps (A,B) = Maps (A9,B9) )
assume A1: ( A = A9 & B = B9 ) ; ::_thesis: Maps (A,B) = Maps (A9,B9)
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Maps_(A,B)_implies_x_in_Maps_(A9,B9)_)_&_(_x_in_Maps_(A9,B9)_implies_x_in_Maps_(A,B)_)_)
let x be set ; ::_thesis: ( ( x in Maps (A,B) implies x in Maps (A9,B9) ) & ( x in Maps (A9,B9) implies x in Maps (A,B) ) )
thus  ( x in Maps (A,B) implies x in Maps (A9,B9) ) ::_thesis: ( x in Maps (A9,B9) implies x in Maps (A,B) )
proof
A2: Maps W c= Maps V by Th7;
assume A3: x in Maps (A,B) ; ::_thesis: x in Maps (A9,B9)
A4: Maps (A,B) c= Maps W by Th17;
then reconsider m = x as Element of Maps W by A3;
A5: m = [[(dom m),(cod m)],(m `2)] by Th8;
 x in Maps W by A3, A4;
then reconsider m9 = x as Element of Maps V by A2;
A6: ( dom m = dom m9 & cod m = cod m9 ) ;
 m = [[A,B],(m `2)] by A3, Th16;
then  ( dom m = A & cod m = B ) by A5, Lm1;
hence  x in Maps (A9,B9) by A1, A6, Th19; ::_thesis: verum
end;
assume A7: x in Maps (A9,B9) ; ::_thesis: x in Maps (A,B)
 Maps (A9,B9) c= Maps V by Th17;
then reconsider m9 = x as Element of Maps V by A7;
A8: m9 = [[A9,B9],(m9 `2)] by A7, Th16;
then A9: m9 `2 is Function of A9,B9 by A7, Lm4;
 ( B9 = {} implies A9 = {} ) by A7, A8, Lm4;
hence  x in Maps (A,B) by A1, A8, A9, Th15; ::_thesis: verum
end;
hence  Maps (A,B) = Maps (A9,B9) by TARSKI:1; ::_thesis: verum
end;

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

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

begin

definition
let V be non empty set ;
func fDom V ->  Function of (Maps V),V means :Def9: :: ENS_1:def 9
 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
deffunc H1( Element of Maps V) ->  Element of V = dom $1;
 ex F being Function of (Maps V),V st
for m being Element of Maps V holds F . m = H1(m) from FUNCT_2:sch_4();
hence  ex b1 being Function of (Maps V),V st
for m being Element of Maps V holds b1 . m = dom m ; ::_thesis: verum
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
let h1, h2 be Function of (Maps V),V; ::_thesis: ( ( for m being Element of Maps V holds h1 . m = dom m ) & ( for m being Element of Maps V holds h2 . m = dom m ) implies h1 = h2 )
assume that
A1: for m being Element of Maps V holds h1 . m = dom m and
A2: for m being Element of Maps V holds h2 . m = dom m ; ::_thesis: h1 = h2
now__::_thesis:_for_m_being_Element_of_Maps_V_holds_h1_._m_=_h2_._m
let m be Element of Maps V; ::_thesis: h1 . m = h2 . m
thus h1 . m = dom m by A1
.= h2 . m by A2 ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:63; ::_thesis: verum
end;
func fCod V ->  Function of (Maps V),V means :Def10: :: ENS_1:def 10
 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
deffunc H1( Element of Maps V) ->  Element of V = cod $1;
 ex F being Function of (Maps V),V st
for m being Element of Maps V holds F . m = H1(m) from FUNCT_2:sch_4();
hence  ex b1 being Function of (Maps V),V st
for m being Element of Maps V holds b1 . m = cod m ; ::_thesis: verum
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
let h1, h2 be Function of (Maps V),V; ::_thesis: ( ( for m being Element of Maps V holds h1 . m = cod m ) & ( for m being Element of Maps V holds h2 . m = cod m ) implies h1 = h2 )
assume that
A3: for m being Element of Maps V holds h1 . m = cod m and
A4: for m being Element of Maps V holds h2 . m = cod m ; ::_thesis: h1 = h2
now__::_thesis:_for_m_being_Element_of_Maps_V_holds_h1_._m_=_h2_._m
let m be Element of Maps V; ::_thesis: h1 . m = h2 . m
thus h1 . m = cod m by A3
.= h2 . m by A4 ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:63; ::_thesis: verum
end;
func fComp V ->  PartFunc of [:(Maps V),(Maps V):],(Maps V) means :Def11: :: ENS_1:def 11
( ( 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
defpred S1[ set , set , set ] means  for m2, m1 being Element of Maps V st m2 = $1 & m1 = $2 holds
( dom m2 = cod m1 & $3 = m2 * m1 );
A5: for x, y, z1, z2 being set st x in Maps V & y in Maps V & S1[x,y,z1] & S1[x,y,z2] holds
z1 = z2
proof
let x, y, z1, z2 be set ; ::_thesis: ( x in Maps V & y in Maps V & S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 )
assume  ( x in Maps V & y in Maps V ) ; ::_thesis: ( not S1[x,y,z1] or not S1[x,y,z2] or z1 = z2 )
then reconsider m2 = x, m1 = y as Element of Maps V ;
assume that
A6: S1[x,y,z1] and
A7: S1[x,y,z2] ; ::_thesis: z1 = z2
 z1 = m2 * m1 by A6;
hence  z1 = z2 by A7; ::_thesis: verum
end;
A8: for x, y, z being set st x in Maps V & y in Maps V & S1[x,y,z] holds
z in Maps V
proof
let x, y, z be set ; ::_thesis: ( x in Maps V & y in Maps V & S1[x,y,z] implies z in Maps V )
assume  ( x in Maps V & y in Maps V ) ; ::_thesis: ( not S1[x,y,z] or z in Maps V )
then reconsider m2 = x, m1 = y as Element of Maps V ;
assume  S1[x,y,z] ; ::_thesis: z in Maps V
then  z = m2 * m1 ;
hence  z in Maps V ; ::_thesis: verum
end;
consider h being PartFunc of [:(Maps V),(Maps V):],(Maps V) such that
A9: for x, y being set holds
( [x,y] in dom h iff ( x in Maps V & y in Maps V & ex z being set st S1[x,y,z] ) ) and
A10: for x, y being set st [x,y] in dom h holds
S1[x,y,h . (x,y)] from BINOP_1:sch_5(A8, A5);
take  h ; ::_thesis: ( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom h iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
h . [m2,m1] = m2 * m1 ) )
thus A11: for m2, m1 being Element of Maps V holds
( [m2,m1] in dom h iff dom m2 = cod m1 ) ::_thesis: for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
h . [m2,m1] = m2 * m1
proof
let m2, m1 be Element of Maps V; ::_thesis: ( [m2,m1] in dom h iff dom m2 = cod m1 )
thus  ( [m2,m1] in dom h implies dom m2 = cod m1 ) ::_thesis: ( dom m2 = cod m1 implies [m2,m1] in dom h )
proof
assume  [m2,m1] in dom h ; ::_thesis: dom m2 = cod m1
then  ex z being set st S1[m2,m1,z] by A9;
hence  dom m2 = cod m1 ; ::_thesis: verum
end;
assume  dom m2 = cod m1 ; ::_thesis: [m2,m1] in dom h
then  S1[m2,m1,m2 * m1] ;
hence  [m2,m1] in dom h by A9; ::_thesis: verum
end;
let m2, m1 be Element of Maps V; ::_thesis: ( dom m2 = cod m1 implies h . [m2,m1] = m2 * m1 )
assume  dom m2 = cod m1 ; ::_thesis: h . [m2,m1] = m2 * m1
then  [m2,m1] in dom h by A11;
then  S1[m2,m1,h . (m2,m1)] by A10;
hence  h . [m2,m1] = m2 * m1 ; ::_thesis: verum
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
let h1, h2 be PartFunc of [:(Maps V),(Maps V):],(Maps V); ::_thesis: ( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom h1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
h1 . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom h2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
h2 . [m2,m1] = m2 * m1 ) implies h1 = h2 )
assume that
A12: for m2, m1 being Element of Maps V holds
( [m2,m1] in dom h1 iff dom m2 = cod m1 ) and
A13: for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
h1 . [m2,m1] = m2 * m1 and
A14: for m2, m1 being Element of Maps V holds
( [m2,m1] in dom h2 iff dom m2 = cod m1 ) and
A15: for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
h2 . [m2,m1] = m2 * m1 ; ::_thesis: h1 = h2
A16: dom h2 c= [:(Maps V),(Maps V):] by RELAT_1:def_18;
A17: dom h1 c= [:(Maps V),(Maps V):] by RELAT_1:def_18;
A18: dom h1 = dom h2
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in dom h1 or [x,y] in dom h2 ) & ( not [x,y] in dom h2 or [x,y] in dom h1 ) )
thus  ( [x,y] in dom h1 implies [x,y] in dom h2 ) ::_thesis: ( not [x,y] in dom h2 or [x,y] in dom h1 )
proof
assume A19: [x,y] in dom h1 ; ::_thesis: [x,y] in dom h2
then reconsider m2 = x, m1 = y as Element of Maps V by A17, ZFMISC_1:87;
 dom m2 = cod m1 by A12, A19;
hence  [x,y] in dom h2 by A14; ::_thesis: verum
end;
assume A20: [x,y] in dom h2 ; ::_thesis: [x,y] in dom h1
then reconsider m2 = x, m1 = y as Element of Maps V by A16, ZFMISC_1:87;
 dom m2 = cod m1 by A14, A20;
hence  [x,y] in dom h1 by A12; ::_thesis: verum
end;
now__::_thesis:_for_m_being_Element_of_[:(Maps_V),(Maps_V):]_st_m_in_dom_h1_holds_
h1_._m_=_h2_._m
let m be Element of [:(Maps V),(Maps V):]; ::_thesis: ( m in dom h1 implies h1 . m = h2 . m )
consider m2, m1 being Element of Maps V such that
A21: m = [m2,m1] by DOMAIN_1:1;
assume  m in dom h1 ; ::_thesis: h1 . m = h2 . m
then A22: dom m2 = cod m1 by A12, A21;
then  h1 . [m2,m1] = m2 * m1 by A13;
hence  h1 . m = h2 . m by A15, A21, A22; ::_thesis: verum
end;
hence  h1 = h2 by A18, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines fDom ENS_1:def_9_:_
 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 Def10 defines fCod ENS_1:def_10_:_
 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 Def11 defines fComp ENS_1:def_11_:_
 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 ) ) );

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

:: deftheorem  ENS_1:def_12_:_
canceled;

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

registration
let V be non empty set ;
cluster Ens V ->  non empty non void strict Category-like transitive associative reflexive with_identities ;
coherence
 ( Ens V is Category-like & Ens V is reflexive & Ens V is transitive & Ens V is associative & Ens V is with_identities )
proof
set M = Maps V;
set d = fDom V;
set c = fCod V;
set p = fComp V;
reconsider C = CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V) #) as non empty non void CatStr ;
A1: C is Category-like
proof
let ff, gg be Morphism of C; :: according to CAT_1:def_6 ::_thesis: ( ( not [gg,ff] in proj1 the Comp of C or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of C ) )
reconsider f = ff, g = gg as Element of Maps V ;
 ( (fDom V) . g = dom g & (fCod V) . f = cod f ) by Def9, Def10;
hence  ( ( not [gg,ff] in proj1 the Comp of C or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of C ) ) by Def11; ::_thesis: verum
end;
A2: C is transitive
proof
let ff, gg be Morphism of C; :: according to CAT_1:def_7 ::_thesis: ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) )
assume A3: dom gg = cod ff ; ::_thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg )
 [gg,ff] in dom the Comp of C by A3, A1, CAT_1:def_6;
then A4: the Comp of C . (gg,ff) = gg (*) ff by CAT_1:def_1;
reconsider f = ff, g = gg as Element of Maps V ;
A5: ( (fDom V) . g = dom g & (fCod V) . f = cod f ) by Def9, Def10;
then A6: (fComp V) . [g,f] = g * f by A3, Def11;
A7: ( (fDom V) . f = dom f & (fCod V) . g = cod g ) by Def9, Def10;
 ( dom (g * f) = dom f & cod (g * f) = cod g ) by A3, A5, Th12;
hence  ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) by A6, A7, Def9, Def10, A4; ::_thesis: verum
end;
A8: C is associative
proof
let ff, gg, hh be Morphism of C; :: according to CAT_1:def_8 ::_thesis: ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff )
assume that
A9: dom hh = cod gg and
A10: dom gg = cod ff ; ::_thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff
reconsider f = ff, g = gg, h = hh as Element of Maps V ;
A11: ( dom h = (fDom V) . h & cod g = (fCod V) . g ) by Def9, Def10;
then A12: dom (h * g) = dom g by A9, Th12;
A13: ( dom g = (fDom V) . g & cod f = (fCod V) . f ) by Def9, Def10;
then A14: cod (g * f) = dom h by A9, A10, A11, Th12;
 [hh,gg] in dom the Comp of C by A9, A1, CAT_1:def_6;
then A15: hh (*) gg = the Comp of C . (hh,gg) by CAT_1:def_1;
 dom (hh (*) gg) = dom gg by A2, CAT_1:def_7, A9;
then A16: [(hh (*) gg),ff] in dom the Comp of C by A1, CAT_1:def_6, A10;
 [gg,ff] in dom the Comp of C by A10, A1, CAT_1:def_6;
then A17: gg (*) ff = the Comp of C . (gg,ff) by CAT_1:def_1;
 cod (gg (*) ff) = cod gg by A2, CAT_1:def_7, A10;
then  [hh,(gg (*) ff)] in dom the Comp of C by A1, CAT_1:def_6, A9;
hence hh (*) (gg (*) ff) = the Comp of C . (hh,( the Comp of C . (gg,ff))) by A17, CAT_1:def_1
.= (fComp V) . [h,(g * f)] by A10, A13, Def11
.= h * (g * f) by A14, Def11
.= (h * g) * f by A9, A10, A11, A13, Th13
.= (fComp V) . [(h * g),f] by A10, A13, A12, Def11
.= the Comp of C . (( the Comp of C . (hh,gg)),ff) by A9, A11, Def11
.= (hh (*) gg) (*) ff by A16, A15, CAT_1:def_1 ;
::_thesis: verum
end;
A18: C is reflexive
proof
let a be Element of C; :: according to CAT_1:def_9 ::_thesis: not Hom (a,a) = {}
reconsider aa = a as Element of V ;
reconsider ii = id$ aa as Morphism of C ;
A19: cod ii = cod (id$ aa) by Def10
.= a by Th11 ;
dom ii = dom (id$ aa) by Def9
.= a by Th11 ;
then  ii in Hom (a,a) by A19;
hence  Hom (a,a) <> {} ; ::_thesis: verum
end;
 C is with_identities
proof
let a be Element of C; :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of C holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
reconsider aa = a as Element of V ;
reconsider ii = id$ aa as Morphism of C ;
A20: cod ii = cod (id$ aa) by Def10
.= a by Th11 ;
A21: dom ii = dom (id$ aa) by Def9
.= a by Th11 ;
then reconsider ii = ii as Morphism of a,a by A20, CAT_1:4;
take  ii ; ::_thesis: for b1 being Element of the carrier of C holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
let b be Element of C; ::_thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
thus  ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) ::_thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )
proof
assume A22: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) ii = g
let g be Morphism of a,b; ::_thesis: g (*) ii = g
reconsider gg = g as Element of Maps V ;
A23: dom gg = dom g by Def9
.= aa by A22, CAT_1:5 ;
then A24: cod (id$ aa) = dom gg by Th11;
 dom g = a by A22, CAT_1:5;
then  [g,ii] in dom (fComp V) by A20, A1, CAT_1:def_6;
hence g (*) ii = (fComp V) . (g,ii) by CAT_1:def_1
.= gg * (id$ aa) by A24, Def11
.= g by A23, Th14 ;
::_thesis: verum
end;
assume A25: Hom (b,a) <> {} ; ::_thesis: for b1 being Morphism of b,a holds ii (*) b1 = b1
let g be Morphism of b,a; ::_thesis: ii (*) g = g
reconsider gg = g as Element of Maps V ;
A26: cod gg = cod g by Def10
.= aa by A25, CAT_1:5 ;
then A27: dom (id$ aa) = cod gg by Th11;
 cod g = a by A25, CAT_1:5;
then  [ii,g] in dom (fComp V) by A21, A1, CAT_1:def_6;
hence ii (*) g = (fComp V) . (ii,g) by CAT_1:def_1
.= (id$ aa) * gg by A27, Def11
.= g by A26, Th14 ;
::_thesis: verum
end;
hence  ( Ens V is Category-like & Ens V is reflexive & Ens V is transitive & Ens V is associative & Ens V is with_identities ) by A1, A2, A8, A18; ::_thesis: verum
end;
end;


theorem :: ENS_1:21
canceled;

theorem :: ENS_1:22
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 14
A;
coherence
 A is Object of (Ens V) ;
end;

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

theorem :: ENS_1:23
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 15
a;
coherence
 a is Element of V ;
end;

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


theorem :: ENS_1:24
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 16
m;
coherence
 m is Morphism of (Ens V) ;
end;

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

theorem :: ENS_1:25
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 17
f;
coherence
 f is Element of Maps V ;
end;

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

theorem :: ENS_1:26
for V being non empty set
for f being Morphism of (Ens V) holds
( dom f = dom (@ f) & cod f = cod (@ f) ) by Def9, Def10;

theorem Th27: :: ENS_1:27
for V being non empty set
for a, b being Object of (Ens V) holds Hom (a,b) = Maps ((@ a),(@ b))
proof
let V be non empty set ; ::_thesis: for a, b being Object of (Ens V) holds Hom (a,b) = Maps ((@ a),(@ b))
let a, b be Object of (Ens V); ::_thesis: Hom (a,b) = Maps ((@ a),(@ b))
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Hom_(a,b)_implies_x_in_Maps_((@_a),(@_b))_)_&_(_x_in_Maps_((@_a),(@_b))_implies_x_in_Hom_(a,b)_)_)
let x be set ; ::_thesis: ( ( x in Hom (a,b) implies x in Maps ((@ a),(@ b)) ) & ( x in Maps ((@ a),(@ b)) implies x in Hom (a,b) ) )
thus  ( x in Hom (a,b) implies x in Maps ((@ a),(@ b)) ) ::_thesis: ( x in Maps ((@ a),(@ b)) implies x in Hom (a,b) )
proof
assume A1: x in Hom (a,b) ; ::_thesis: x in Maps ((@ a),(@ b))
then reconsider f = x as Morphism of (Ens V) ;
 cod f = b by A1, CAT_1:1;
then A2: cod (@ f) = @ b by Def10;
 dom f = a by A1, CAT_1:1;
then  dom (@ f) = @ a by Def9;
hence  x in Maps ((@ a),(@ b)) by A2, Th19; ::_thesis: verum
end;
assume A3: x in Maps ((@ a),(@ b)) ; ::_thesis: x in Hom (a,b)
 Maps ((@ a),(@ b)) c= Maps V by Th17;
then reconsider m = x as Element of Maps V by A3;
 cod m = @ b by A3, Th19;
then A4: cod (@ m) = b by Def10;
 dom m = @ a by A3, Th19;
then  dom (@ m) = a by Def9;
hence  x in Hom (a,b) by A4; ::_thesis: verum
end;
hence  Hom (a,b) = Maps ((@ a),(@ b)) by TARSKI:1; ::_thesis: verum
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
let V be non empty set ; ::_thesis: for a, b being Object of (Ens V) st Hom (a,b) <> {} holds
Funcs ((@ a),(@ b)) <> {}
let a, b be Object of (Ens V); ::_thesis: ( Hom (a,b) <> {} implies Funcs ((@ a),(@ b)) <> {} )
set m = the Element of Maps ((@ a),(@ b));
assume  Hom (a,b) <> {} ; ::_thesis: Funcs ((@ a),(@ b)) <> {}
then A1: Maps ((@ a),(@ b)) <> {} by Th27;
reconsider m = the Element of Maps ((@ a),(@ b)) as Element of Maps V by A1, TARSKI:def_3, Th17;
 m `2 in Funcs ((@ a),(@ b)) by A1, Th20;
hence  Funcs ((@ a),(@ b)) <> {} ; ::_thesis: verum
end;

theorem Th28: :: ENS_1:28
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
let V be non empty set ; ::_thesis: for g, f being Morphism of (Ens V) st dom g = cod f holds
g (*) f = (@ g) * (@ f)
let g, f be Morphism of (Ens V); ::_thesis: ( dom g = cod f implies g (*) f = (@ g) * (@ f) )
assume A1: dom g = cod f ; ::_thesis: g (*) f = (@ g) * (@ f)
then  dom (@ g) = cod f by Def9;
then A2: dom (@ g) = cod (@ f) by Def10;
thus g (*) f = the Comp of (Ens V) . ((@ g),f) by A1, CAT_1:16
.= (@ g) * (@ f) by A2, Def11 ; ::_thesis: verum
end;

theorem Th29: :: ENS_1:29
for V being non empty set
for a being Object of (Ens V) holds id a = id$ (@ a)
proof
let V be non empty set ; ::_thesis: for a being Object of (Ens V) holds id a = id$ (@ a)
let a be Object of (Ens V); ::_thesis: id a = id$ (@ a)
reconsider aa = a as Element of V ;
reconsider ii = id$ aa as Morphism of (Ens V) ;
A1: cod ii = cod (id$ aa) by Def10
.= a by Th11 ;
A2: dom ii = dom (id$ aa) by Def9
.= a by Th11 ;
then reconsider ii = ii as Morphism of a,a by A1, CAT_1:4;
 for b being Object of (Ens V) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
proof
let b be Element of (Ens V); ::_thesis: ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
set p = the Comp of (Ens V);
thus  ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f )
proof
assume A3: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) ii = g
let g be Morphism of a,b; ::_thesis: g (*) ii = g
reconsider gg = g as Element of Maps V ;
A4: dom gg = dom g by Def9
.= aa by A3, CAT_1:5 ;
then A5: cod (id$ aa) = dom gg by Th11;
 dom g = a by A3, CAT_1:5;
then  [g,ii] in dom the Comp of (Ens V) by A1, CAT_1:def_6;
hence g (*) ii = the Comp of (Ens V) . (g,ii) by CAT_1:def_1
.= gg * (id$ aa) by A5, Def11
.= g by A4, Th14 ;
::_thesis: verum
end;
assume A6: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds ii (*) f = f
let g be Morphism of b,a; ::_thesis: ii (*) g = g
reconsider gg = g as Element of Maps V ;
A7: cod gg = cod g by Def10
.= aa by A6, CAT_1:5 ;
then A8: dom (id$ aa) = cod gg by Th11;
 cod g = a by A6, CAT_1:5;
then  [ii,g] in dom the Comp of (Ens V) by A2, CAT_1:def_6;
hence ii (*) g = the Comp of (Ens V) . (ii,g) by CAT_1:def_1
.= (id$ aa) * gg by A8, Def11
.= g by A7, Th14 ;
::_thesis: verum
end;
hence  id a = id$ (@ a) by CAT_1:def_12; ::_thesis: verum
end;

theorem :: ENS_1:30
for V being non empty set
for a being Object of (Ens V) st a = {} holds
a is initial
proof
let V be non empty set ; ::_thesis: for a being Object of (Ens V) st a = {} holds
a is initial
let a be Object of (Ens V); ::_thesis: ( a = {} implies a is initial )
assume A1: a = {} ; ::_thesis: a is initial
let b be Object of (Ens V); :: according to CAT_1:def_19 ::_thesis: ( not Hom (a,b) = {} & ex b1 being Morphism of a,b st
for b2 being Morphism of a,b holds b1 = b2 )
 Maps ((@ a),(@ b)) <> {} by A1, Th15;
hence A2: Hom (a,b) <> {} by Th27; ::_thesis: ex b1 being Morphism of a,b st
for b2 being Morphism of a,b holds b1 = b2
set m = [[(@ a),(@ b)],{}];
 {} is Function of (@ a),(@ b) by A1, RELSET_1:12;
then  [[(@ a),(@ b)],{}] in Maps ((@ a),(@ b)) by A1, Th15;
then  [[(@ a),(@ b)],{}] in Hom (a,b) by Th27;
then reconsider f = [[(@ a),(@ b)],{}] as Morphism of a,b by CAT_1:def_5;
take  f ; ::_thesis: for b1 being Morphism of a,b holds f = b1
let g be Morphism of a,b; ::_thesis: f = g
reconsider m9 = g as Element of Maps V ;
 g in Hom (a,b) by A2, CAT_1:def_5;
then A3: g in Maps ((@ a),(@ b)) by Th27;
then A4: m9 = [[(@ a),(@ b)],(m9 `2)] by Th16;
then  m9 `2 is Function of (@ a),(@ b) by A3, Lm4;
hence  f = g by A1, A4; ::_thesis: verum
end;

theorem Th31: :: ENS_1:31
for V being non empty set
for a being Object of (Ens V) st {} in V & a is initial holds
a = {}
proof
let V be non empty set ; ::_thesis: for a being Object of (Ens V) st {} in V & a is initial holds
a = {}
let a be Object of (Ens V); ::_thesis: ( {} in V & a is initial implies a = {} )
assume  {} in V ; ::_thesis: ( not a is initial or a = {} )
then reconsider B = {} as Element of V ;
set b = @ B;
assume  a is initial ; ::_thesis: a = {}
then  Hom (a,(@ B)) <> {} by CAT_1:def_19;
then  Funcs ((@ a),(@ (@ B))) <> {} by Lm6;
hence  a = {} ; ::_thesis: verum
end;

theorem :: ENS_1:32
for W being Universe
for a being Object of (Ens W) st a is initial holds
a = {} by Th31, CLASSES2:56;

theorem :: ENS_1:33
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
let V be non empty set ; ::_thesis: for a being Object of (Ens V) st ex x being set st a = {x} holds
a is terminal
let a be Object of (Ens V); ::_thesis: ( ex x being set st a = {x} implies a is terminal )
given x being set  such that A1: a = {x} ; ::_thesis: a is terminal
let b be Object of (Ens V); :: according to CAT_1:def_18 ::_thesis: ( not Hom (b,a) = {} & ex b1 being Morphism of b,a st
for b2 being Morphism of b,a holds b1 = b2 )
set h = the Function of (@ b),(@ a);
set m = [[(@ b),(@ a)], the Function of (@ b),(@ a)];
A2: [[(@ b),(@ a)], the Function of (@ b),(@ a)] in Maps ((@ b),(@ a)) by A1, Th15;
hence A3: Hom (b,a) <> {} by Th27; ::_thesis: ex b1 being Morphism of b,a st
for b2 being Morphism of b,a holds b1 = b2
 [[(@ b),(@ a)], the Function of (@ b),(@ a)] in Hom (b,a) by A2, Th27;
then reconsider f = [[(@ b),(@ a)], the Function of (@ b),(@ a)] as Morphism of b,a by CAT_1:def_5;
take  f ; ::_thesis: for b1 being Morphism of b,a holds f = b1
let g be Morphism of b,a; ::_thesis: f = g
reconsider m9 = g as Element of Maps V ;
 g in Hom (b,a) by A3, CAT_1:def_5;
then A4: g in Maps ((@ b),(@ a)) by Th27;
then A5: m9 = [[(@ b),(@ a)],(m9 `2)] by Th16;
then  m9 `2 is Function of (@ b),(@ a) by A4, Lm4;
hence  f = g by A1, A5, FUNCT_2:51; ::_thesis: verum
end;

theorem Th34: :: ENS_1:34
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
let V be non empty set ; ::_thesis: for a being Object of (Ens V) st V <> {{}} & a is terminal holds
ex x being set st a = {x}
let a be Object of (Ens V); ::_thesis: ( V <> {{}} & a is terminal implies ex x being set st a = {x} )
assume that
A1: V <> {{}} and
A2: a is terminal ; ::_thesis: ex x being set st a = {x}
set x = the Element of @ a;
A3: now__::_thesis:_not_@_a_=_{}
assume A4: @ a = {} ; ::_thesis: contradiction
now__::_thesis:_contradiction
consider C being set  such that
A5: C in V and
A6: C <> {} by A1, ZFMISC_1:35;
reconsider C = C as Element of V by A5;
set b = @ C;
 Hom ((@ C),a) <> {} by A2, CAT_1:def_18;
then  Funcs ((@ (@ C)),(@ a)) <> {} by Lm6;
hence  contradiction by A4, A6; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;
now__::_thesis:_not_a_<>_{_the_Element_of_@_a}
assume  a <> { the Element of @ a} ; ::_thesis: contradiction
then consider y being set  such that
A7: y in @ a and
A8: y <> the Element of @ a by A3, ZFMISC_1:35;
reconsider fy = (@ a) --> y as Function of (@ a),(@ a) by A7, FUNCOP_1:45;
reconsider fx = (@ a) --> the Element of @ a as Function of (@ a),(@ a) by A7, FUNCOP_1:45;
 fx . y = the Element of @ a by A7, FUNCOP_1:7;
then A9: fx <> fy by A7, A8, FUNCOP_1:7;
A10: [[(@ a),(@ a)],fx] in Maps ((@ a),(@ a)) by Th15;
A11: [[(@ a),(@ a)],fy] in Maps ((@ a),(@ a)) by Th15;
 Maps ((@ a),(@ a)) c= Maps V by Th17;
then reconsider m1 = [[(@ a),(@ a)],fx], m2 = [[(@ a),(@ a)],fy] as Element of Maps V by A10, A11;
A12: m2 in Hom (a,a) by A11, Th27;
 m1 in Hom (a,a) by A10, Th27;
then reconsider f = @ m1, g = @ m2 as Morphism of a,a by A12, CAT_1:def_5;
consider h being Morphism of a,a such that
A13: for h9 being Morphism of a,a holds h = h9 by A2, CAT_1:def_18;
f = h by A13
.= g by A13 ;
hence  contradiction by A9, XTUPLE_0:1; ::_thesis: verum
end;
hence  ex x being set st a = {x} ; ::_thesis: verum
end;

theorem :: ENS_1:35
for W being Universe
for a being Object of (Ens W) st a is terminal holds
ex x being set st a = {x}
proof
let W be Universe; ::_thesis: for a being Object of (Ens W) st a is terminal holds
ex x being set st a = {x}
let a be Object of (Ens W); ::_thesis: ( a is terminal implies ex x being set st a = {x} )
now__::_thesis:_not_W_=_{{}}
A1: {{}} in W by CLASSES2:56, CLASSES2:57;
assume  W = {{}} ; ::_thesis: contradiction
hence  contradiction by A1; ::_thesis: verum
end;
hence  ( a is terminal implies ex x being set st a = {x} ) by Th34; ::_thesis: verum
end;

theorem :: ENS_1:36
for V being non empty set
for a, b being Object of (Ens V)
for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is monic iff (@ f) `2 is one-to-one )
proof
let V be non empty set ; ::_thesis: for a, b being Object of (Ens V)
for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is monic iff (@ f) `2 is one-to-one )
let a, b be Object of (Ens V); ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is monic iff (@ f) `2 is one-to-one )
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies ( f is monic iff (@ f) `2 is one-to-one ) )
assume A1: Hom (a,b) <> {} ; ::_thesis: ( f is monic iff (@ f) `2 is one-to-one )
set m = @ f;
A2: dom (@ f) = dom f by Def9;
then A3: dom ((@ f) `2) = dom f by Lm3;
thus  ( f is monic implies (@ f) `2 is one-to-one ) ::_thesis: ( (@ f) `2 is one-to-one implies f is monic )
proof
set A = dom ((@ f) `2);
assume A4: f is monic ; ::_thesis: (@ f) `2 is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 ((@ f) `2) or not x2 in proj1 ((@ f) `2) or not ((@ f) `2) . x1 = ((@ f) `2) . x2 or x1 = x2 )
assume that
A5: x1 in dom ((@ f) `2) and
A6: x2 in dom ((@ f) `2) and
A7: ((@ f) `2) . x1 = ((@ f) `2) . x2 ; ::_thesis: x1 = x2
A8: dom ((@ f) `2) = dom (@ f) by Lm3;
then reconsider A = dom ((@ f) `2) as Element of V ;
A9: dom f = A by A8, Def9;
reconsider fx1 = A --> x1, fx2 = A --> x2 as Function of A,A by A5, A6, FUNCOP_1:45;
reconsider m1 = [[A,A],fx1], m2 = [[A,A],fx2] as Element of Maps V by Th5;
set f1 = @ m1;
set f2 = @ m2;
set h1 = ((@ f) `2) * ((@ (@ m1)) `2);
set h2 = ((@ f) `2) * ((@ (@ m2)) `2);
set ff1 = (@ f) * (@ (@ m1));
set ff2 = (@ f) * (@ (@ m2));
A10: m2 = [[(dom m2),(cod m2)],(m2 `2)] by Th8;
then A11: dom m2 = A by Lm1;
A12: cod m2 = A by A10, Lm1;
then A13: ( ((@ f) * (@ (@ m2))) `2 = ((@ f) `2) * ((@ (@ m2)) `2) & dom ((@ f) * (@ (@ m2))) = dom (@ (@ m2)) ) by A8, Th12;
 cod ((@ f) * (@ (@ m2))) = cod (@ f) by A8, A12, Th12;
then A14: (@ f) * (@ (@ m2)) = [[(dom (@ (@ m2))),(cod (@ f))],(((@ f) `2) * ((@ (@ m2)) `2))] by A13, Th8;
 dom (@ (@ m2)) = A by A10, Lm1;
then A15: dom (@ m2) = A by Def9;
 cod (@ (@ m2)) = A by A10, Lm1;
then A16: cod (@ m2) = A by Def10;
then A17: f (*) (@ m2) = (@ f) * (@ (@ m2)) by A9, Th28;
A18: m1 = [[(dom m1),(cod m1)],(m1 `2)] by Th8;
then A19: cod m1 = A by Lm1;
then A20: ( ((@ f) * (@ (@ m1))) `2 = ((@ f) `2) * ((@ (@ m1)) `2) & dom ((@ f) * (@ (@ m1))) = dom (@ (@ m1)) ) by A8, Th12;
A21: dom m1 = A by A18, Lm1;
now__::_thesis:_(_dom_(((@_f)_`2)_*_((@_(@_m1))_`2))_=_A_&_dom_(((@_f)_`2)_*_((@_(@_m2))_`2))_=_A_&_(_for_x_being_set_st_x_in_A_holds_
(((@_f)_`2)_*_((@_(@_m1))_`2))_._x_=_(((@_f)_`2)_*_((@_(@_m2))_`2))_._x_)_)
thus A22: ( dom (((@ f) `2) * ((@ (@ m1)) `2)) = A & dom (((@ f) `2) * ((@ (@ m2)) `2)) = A ) by A21, A11, A20, A13, Lm3; ::_thesis: for x being set st x in A holds
(((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x
let x be set ; ::_thesis: ( x in A implies (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x )
assume A23: x in A ; ::_thesis: (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x
 fx1 = m1 `2 by A18, XTUPLE_0:1;
then  ((@ (@ m1)) `2) . x = x1 by A23, FUNCOP_1:7;
then A24: (((@ f) `2) * ((@ (@ m1)) `2)) . x = ((@ f) `2) . x1 by A22, A23, FUNCT_1:12;
 fx2 = m2 `2 by A10, XTUPLE_0:1;
then  ((@ (@ m2)) `2) . x = x2 by A23, FUNCOP_1:7;
hence  (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x by A7, A22, A23, A24, FUNCT_1:12; ::_thesis: verum
end;
then A25: ((@ f) `2) * ((@ (@ m1)) `2) = ((@ f) `2) * ((@ (@ m2)) `2) by FUNCT_1:2;
 cod ((@ f) * (@ (@ m1))) = cod (@ f) by A8, A19, Th12;
then A26: (@ f) * (@ (@ m1)) = [[(dom (@ (@ m1))),(cod (@ f))],(((@ f) `2) * ((@ (@ m1)) `2))] by A20, Th8;
 dom (@ (@ m1)) = A by A18, Lm1;
then A27: dom (@ m1) = A by Def9;
 cod (@ (@ m1)) = A by A18, Lm1;
then A28: cod (@ m1) = A by Def10;
reconsider A = A as Object of (Ens V) ;
A29: dom f = a by A1, CAT_1:5;
then A30: ( @ m1 in Hom (A,a) & @ m2 in Hom (A,a) ) by A27, A9, A28, A15, A16;
then reconsider f1 = @ m1, f2 = @ m2 as Morphism of A,a by CAT_1:def_5;
A31: f * f1 = f (*) f1 by A1, A30, CAT_1:def_13
.= f (*) f2 by A21, A11, A26, A14, A25, A17, A28, A9, Th28
.= f * f2 by A1, A30, CAT_1:def_13 ;
 Hom (A,a) <> {} by A29, A9;
then  f1 = f2 by A4, A31, CAT_1:def_14;
then  fx1 = fx2 by XTUPLE_0:1;
hence x1 = fx2 . x1 by A5, FUNCOP_1:7
.= x2 by A5, FUNCOP_1:7 ;
::_thesis: verum
end;
assume A32: (@ f) `2 is one-to-one ; ::_thesis: f is monic
thus  Hom (a,b) <> {} by A1; :: according to CAT_1:def_14 ::_thesis: for b1 being Element of the carrier of (Ens V) holds
( Hom (b1,a) = {} or for b2, b3 being Morphism of b1,a holds
( not f * b2 = f * b3 or b2 = b3 ) )
let c be Object of (Ens V); ::_thesis: ( Hom (c,a) = {} or for b1, b2 being Morphism of c,a holds
( not f * b1 = f * b2 or b1 = b2 ) )
assume A33: Hom (c,a) <> {} ; ::_thesis: for b1, b2 being Morphism of c,a holds
( not f * b1 = f * b2 or b1 = b2 )
let f1, f2 be Morphism of c,a; ::_thesis: ( not f * f1 = f * f2 or f1 = f2 )
A34: dom f1 = c by A33, CAT_1:5
.= dom f2 by A33, CAT_1:5 ;
A35: cod f1 = a by A33, CAT_1:5
.= dom f by A1, CAT_1:5 ;
A36: cod f2 = a by A33, CAT_1:5
.= dom f by A1, CAT_1:5 ;
assume A37: f * f1 = f * f2 ; ::_thesis: f1 = f2
set m1 = @ f1;
set m2 = @ f2;
A38: (@ f) * (@ f1) = f (*) f1 by A35, Th28
.= f * f1 by A33, A1, CAT_1:def_13 ;
A39: (@ f) * (@ f2) = f (*) f2 by A36, Th28
.= f * f2 by A33, A1, CAT_1:def_13 ;
A40: @ f1 = [[(dom (@ f1)),(cod (@ f1))],((@ f1) `2)] by Th8;
A41: dom (@ f2) = dom f2 by Def9;
then A42: dom ((@ f2) `2) = dom f2 by Lm3;
A43: cod (@ f1) = cod f1 by Def10;
then A44: rng ((@ f1) `2) c= cod f1 by Lm3;
A45: cod (@ f2) = cod f2 by Def10;
then A46: rng ((@ f2) `2) c= cod f2 by Lm3;
A47: (@ f) * (@ f2) = [[(dom (@ f2)),(cod (@ f))],(((@ f) `2) * ((@ f2) `2))] by A36, A45, A2, Def6;
 (@ f) * (@ f1) = [[(dom (@ f1)),(cod (@ f))],(((@ f) `2) * ((@ f1) `2))] by A35, A43, A2, Def6;
then A48: ((@ f) `2) * ((@ f1) `2) = ((@ f) `2) * ((@ f2) `2) by A39, A37, A38, A47, XTUPLE_0:1;
A49: dom (@ f1) = dom f1 by Def9;
then  dom ((@ f1) `2) = dom f1 by Lm3;
then  (@ f1) `2 = (@ f2) `2 by A32, A34, A35, A36, A42, A3, A44, A46, A48, FUNCT_1:27;
hence  f1 = f2 by A34, A35, A36, A49, A41, A43, A45, A40, Th8; ::_thesis: verum
end;

theorem Th37: :: ENS_1:37
for V being non empty set
for a, b being Object of (Ens V)
for f being Morphism of a,b st Hom (a,b) <> {} & 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
let V be non empty set ; ::_thesis: for a, b being Object of (Ens V)
for f being Morphism of a,b st Hom (a,b) <> {} & 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
let a, b be Object of (Ens V); ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} & 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
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} & f is epi & ex A being Element of V ex x1, x2 being set st
( x1 in A & x2 in A & x1 <> x2 ) implies @ f is surjective )
assume A1: Hom (a,b) <> {} ; ::_thesis: ( not f is epi or for A being Element of V
for x1, x2 being set holds
( not x1 in A or not x2 in A or not x1 <> x2 ) or @ f is surjective )
assume A2: f is epi ; ::_thesis: ( for A being Element of V
for x1, x2 being set holds
( not x1 in A or not x2 in A or not x1 <> x2 ) or @ f is surjective )
given B being Element of V, x1, x2 being set  such that A3: x1 in B and
A4: x2 in B and
A5: x1 <> x2 ; ::_thesis: @ f is surjective
A6: cod (@ f) c= rng ((@ f) `2)
proof
set A = cod (@ f);
reconsider g1 = (cod (@ f)) --> x1 as Function of (cod (@ f)),B by A3, FUNCOP_1:45;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cod (@ f) or x in rng ((@ f) `2) )
assume that
A7: x in cod (@ f) and
A8: not x in rng ((@ f) `2) ; ::_thesis: contradiction
set h = {x} --> x2;
set g2 = g1 +* ({x} --> x2);
A9: dom ({x} --> x2) = {x} by FUNCOP_1:13;
A10: rng ({x} --> x2) = {x2} by FUNCOP_1:8;
 rng g1 = {x1} by A7, FUNCOP_1:8;
then  rng (g1 +* ({x} --> x2)) c= {x1} \/ {x2} by A10, FUNCT_4:17;
then A11: rng (g1 +* ({x} --> x2)) c= {x1,x2} by ENUMSET1:1;
 {x1,x2} c= B by A3, A4, ZFMISC_1:32;
then A12: rng (g1 +* ({x} --> x2)) c= B by A11, XBOOLE_1:1;
 dom g1 = cod (@ f) by FUNCOP_1:13;
then  dom (g1 +* ({x} --> x2)) = (cod (@ f)) \/ {x} by A9, FUNCT_4:def_1
.= cod (@ f) by A7, ZFMISC_1:40 ;
then reconsider g2 = g1 +* ({x} --> x2) as Function of (cod (@ f)),B by A3, A12, FUNCT_2:def_1, RELSET_1:4;
A13: cod f = cod (@ f) by Def10;
A14: x in {x} by TARSKI:def_1;
then  ({x} --> x2) . x = x2 by FUNCOP_1:7;
then A15: g2 . x = x2 by A14, A9, FUNCT_4:13;
A16: g1 . x = x1 by A7, FUNCOP_1:7;
reconsider m1 = [[(cod (@ f)),B],g1], m2 = [[(cod (@ f)),B],g2] as Element of Maps V by A3, Th5;
set f1 = @ m1;
set f2 = @ m2;
set h1 = ((@ (@ m1)) `2) * ((@ f) `2);
set h2 = ((@ (@ m2)) `2) * ((@ f) `2);
set f1f = (@ (@ m1)) * (@ f);
set f2f = (@ (@ m2)) * (@ f);
A17: m1 = [[(dom m1),(cod m1)],(m1 `2)] by Th8;
then A18: g1 = m1 `2 by XTUPLE_0:1;
A19: dom m1 = cod (@ f) by A17, Lm1;
then A20: ( ((@ (@ m1)) * (@ f)) `2 = ((@ (@ m1)) `2) * ((@ f) `2) & dom ((@ (@ m1)) * (@ f)) = dom (@ f) ) by Th12;
A21: m2 = [[(dom m2),(cod m2)],(m2 `2)] by Th8;
then A22: dom m2 = cod (@ f) by Lm1;
then A23: ( ((@ (@ m2)) * (@ f)) `2 = ((@ (@ m2)) `2) * ((@ f) `2) & dom ((@ (@ m2)) * (@ f)) = dom (@ f) ) by Th12;
 cod (@ (@ m2)) = B by A21, Lm1;
then A24: cod (@ m2) = B by Def10;
 dom (@ (@ m2)) = cod (@ f) by A21, Lm1;
then A25: dom (@ m2) = cod (@ f) by Def9;
then A26: (@ m2) (*) f = (@ (@ m2)) * (@ f) by A13, Th28;
A27: g2 = m2 `2 by A21, XTUPLE_0:1;
now__::_thesis:_(_dom_(((@_(@_m1))_`2)_*_((@_f)_`2))_=_dom_(@_f)_&_dom_(((@_(@_m2))_`2)_*_((@_f)_`2))_=_dom_(@_f)_&_(_for_z_being_set_st_z_in_dom_(@_f)_holds_
(((@_(@_m1))_`2)_*_((@_f)_`2))_._z_=_(((@_(@_m2))_`2)_*_((@_f)_`2))_._z_)_)
thus A28: ( dom (((@ (@ m1)) `2) * ((@ f) `2)) = dom (@ f) & dom (((@ (@ m2)) `2) * ((@ f) `2)) = dom (@ f) ) by A20, A23, Lm3; ::_thesis: for z being set st z in dom (@ f) holds
(((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z
let z be set ; ::_thesis: ( z in dom (@ f) implies (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z )
set y = ((@ f) `2) . z;
assume A29: z in dom (@ f) ; ::_thesis: (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z
then  z in dom ((@ f) `2) by Lm3;
then  ((@ f) `2) . z in rng ((@ f) `2) by FUNCT_1:def_3;
then A30: not ((@ f) `2) . z in {x} by A8, TARSKI:def_1;
 ( (((@ (@ m1)) `2) * ((@ f) `2)) . z = g1 . (((@ f) `2) . z) & (((@ (@ m2)) `2) * ((@ f) `2)) . z = g2 . (((@ f) `2) . z) ) by A18, A27, A28, A29, FUNCT_1:12;
hence  (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z by A9, A30, FUNCT_4:11; ::_thesis: verum
end;
then A31: ((@ (@ m1)) `2) * ((@ f) `2) = ((@ (@ m2)) `2) * ((@ f) `2) by FUNCT_1:2;
 cod ((@ (@ m1)) * (@ f)) = cod (@ (@ m1)) by A19, Th12;
then A32: (@ (@ m1)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m1)))],(((@ (@ m1)) `2) * ((@ f) `2))] by A20, Th8;
 cod ((@ (@ m2)) * (@ f)) = cod (@ (@ m2)) by A22, Th12;
then A33: (@ (@ m2)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m2)))],(((@ (@ m2)) `2) * ((@ f) `2))] by A23, Th8;
 cod m1 = B by A17, Lm1;
then A34: (@ (@ m1)) * (@ f) = (@ (@ m2)) * (@ f) by A21, A32, A33, A31, Lm1;
 cod (@ (@ m1)) = B by A17, Lm1;
then A35: cod (@ m1) = B by Def10;
 dom (@ (@ m1)) = cod (@ f) by A17, Lm1;
then A36: dom (@ m1) = cod (@ f) by Def9;
reconsider B = B as Object of (Ens V) ;
A37: cod f = b by A1, CAT_1:5;
then A38: @ m1 in Hom (b,B) by A13, A35, A36;
then reconsider f1 = @ m1 as Morphism of b,B by CAT_1:def_5;
 @ m2 in Hom (b,B) by A13, A24, A25, A37;
then reconsider f2 = @ m2 as Morphism of b,B by CAT_1:def_5;
f1 * f = f1 (*) f by A1, A38, CAT_1:def_13
.= f2 (*) f by A34, A26, A36, A13, Th28
.= f2 * f by A1, A38, CAT_1:def_13 ;
then  f1 = f2 by A2, A38, CAT_1:def_15;
hence  contradiction by A5, A16, A15, XTUPLE_0:1; ::_thesis: verum
end;
 rng ((@ f) `2) c= cod (@ f) by Lm3;
hence  rng ((@ f) `2) = cod (@ f) by A6, XBOOLE_0:def_10; :: according to ENS_1:def_8 ::_thesis: verum
end;

theorem :: ENS_1:38
for V being non empty set
for a, b being Object of (Ens V) st Hom (a,b) <> {} holds
for f being Morphism of a,b st @ f is surjective holds
f is epi
proof
let V be non empty set ; ::_thesis: for a, b being Object of (Ens V) st Hom (a,b) <> {} holds
for f being Morphism of a,b st @ f is surjective holds
f is epi
let a, b be Object of (Ens V); ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b st @ f is surjective holds
f is epi )
assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b st @ f is surjective holds
f is epi
let f be Morphism of a,b; ::_thesis: ( @ f is surjective implies f is epi )
set m = @ f;
assume A2: rng ((@ f) `2) = cod (@ f) ; :: according to ENS_1:def_8 ::_thesis: f is epi
thus  Hom (a,b) <> {} by A1; :: according to CAT_1:def_15 ::_thesis: for b1 being Element of the carrier of (Ens V) holds
( Hom (b,b1) = {} or for b2, b3 being Morphism of b,b1 holds
( not b2 * f = b3 * f or b2 = b3 ) )
let c be Object of (Ens V); ::_thesis: ( Hom (b,c) = {} or for b1, b2 being Morphism of b,c holds
( not b1 * f = b2 * f or b1 = b2 ) )
assume A3: Hom (b,c) <> {} ; ::_thesis: for b1, b2 being Morphism of b,c holds
( not b1 * f = b2 * f or b1 = b2 )
let f1, f2 be Morphism of b,c; ::_thesis: ( not f1 * f = f2 * f or f1 = f2 )
A4: dom f1 = b by A3, CAT_1:5
.= cod f by A1, CAT_1:5 ;
A5: dom f2 = b by A3, CAT_1:5
.= cod f by A1, CAT_1:5 ;
A6: cod f1 = c by A3, CAT_1:5
.= cod f2 by A3, CAT_1:5 ;
assume A7: f1 * f = f2 * f ; ::_thesis: f1 = f2
set m1 = @ f1;
set m2 = @ f2;
A8: (@ f1) * (@ f) = f1 (*) f by A4, Th28
.= f1 * f by A1, A3, CAT_1:def_13 ;
A9: (@ f2) * (@ f) = f2 (*) f by A5, Th28
.= f2 * f by A1, A3, CAT_1:def_13 ;
A10: @ f1 = [[(dom (@ f1)),(cod (@ f1))],((@ f1) `2)] by Th8;
A11: ( cod (@ f1) = cod f1 & cod (@ f2) = cod f2 ) by Def10;
A12: dom (@ f2) = dom f2 by Def9;
then A13: dom ((@ f2) `2) = dom f2 by Lm3;
A14: cod (@ f) = cod f by Def10;
then A15: (@ f2) * (@ f) = [[(dom (@ f)),(cod (@ f2))],(((@ f2) `2) * ((@ f) `2))] by A5, A12, Def6;
A16: dom (@ f1) = dom f1 by Def9;
then  (@ f1) * (@ f) = [[(dom (@ f)),(cod (@ f1))],(((@ f1) `2) * ((@ f) `2))] by A4, A14, Def6;
then A17: ((@ f1) `2) * ((@ f) `2) = ((@ f2) `2) * ((@ f) `2) by A7, A8, A15, A9, XTUPLE_0:1;
 dom ((@ f1) `2) = dom f1 by A16, Lm3;
then  (@ f1) `2 = (@ f2) `2 by A2, A4, A5, A14, A17, A13, FUNCT_1:86;
hence  f1 = f2 by A4, A5, A6, A16, A12, A11, A10, Th8; ::_thesis: verum
end;

theorem :: ENS_1:39
for W being Universe
for a, b being Object of (Ens W) st Hom (a,b) <> {} holds
for f being Morphism of a,b st f is epi holds
@ f is surjective
proof
let W be Universe; ::_thesis: for a, b being Object of (Ens W) st Hom (a,b) <> {} holds
for f being Morphism of a,b st f is epi holds
@ f is surjective
let a, b be Object of (Ens W); ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b st f is epi holds
@ f is surjective )
assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b st f is epi holds
@ f is surjective
let f be Morphism of a,b; ::_thesis: ( f is epi implies @ f is surjective )
 ( {} in W & {{}} in W ) by CLASSES2:56, CLASSES2:57;
then A2: {{},{{}}} in W by CLASSES2:58;
 ( {} in {{},{{}}} & {{}} in {{},{{}}} ) by TARSKI:def_2;
hence  ( f is epi implies @ f is surjective ) by A2, Th37, A1; ::_thesis: verum
end;

Lm7:  for V being non empty set
for W being non empty Subset of V holds Ens W is Subcategory of Ens V
proof
let V be non empty set ; ::_thesis: for W being non empty Subset of V holds Ens W is Subcategory of Ens V
let W be non empty Subset of V; ::_thesis: Ens W is Subcategory of Ens V
A1: for a, b being Object of (Ens W)
for a9, b9 being Object of (Ens V) st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
proof
let a, b be Object of (Ens W); ::_thesis: for a9, b9 being Object of (Ens V) st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
let a9, b9 be Object of (Ens V); ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )
assume A2: ( a = a9 & b = b9 ) ; ::_thesis: Hom (a,b) = Hom (a9,b9)
 ( Hom (a,b) = Maps ((@ a),(@ b)) & Hom (a9,b9) = Maps ((@ a9),(@ b9)) ) by Th27;
hence  Hom (a,b) = Hom (a9,b9) by A2, Lm5; ::_thesis: verum
end;
set w = the Comp of (Ens W);
set v = the Comp of (Ens V);
thus  the carrier of (Ens W) c= the carrier of (Ens V) ; :: according to CAT_2:def_4 ::_thesis: ( ( for b1, b2 being Element of the carrier of (Ens W)
for b3, b4 being Element of the carrier of (Ens V) holds
( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of (Ens W) c= the Comp of (Ens V) & ( for b1 being Element of the carrier of (Ens W)
for b2 being Element of the carrier of (Ens V) holds
( not b1 = b2 or id b1 = id b2 ) ) )
thus  for a, b being Object of (Ens W)
for a9, b9 being Object of (Ens V) st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) by A1; ::_thesis: ( the Comp of (Ens W) c= the Comp of (Ens V) & ( for b1 being Element of the carrier of (Ens W)
for b2 being Element of the carrier of (Ens V) holds
( not b1 = b2 or id b1 = id b2 ) ) )
now__::_thesis:_(_dom_the_Comp_of_(Ens_W)_c=_dom_the_Comp_of_(Ens_V)_&_(_for_x_being_set_st_x_in_dom_the_Comp_of_(Ens_W)_holds_
the_Comp_of_(Ens_W)_._x_=_the_Comp_of_(Ens_V)_._x_)_)
A3: dom the Comp of (Ens W) c= [:(Maps W),(Maps W):] by RELAT_1:def_18;
thus A4: dom the Comp of (Ens W) c= dom the Comp of (Ens V) ::_thesis: for x being set st x in dom the Comp of (Ens W) holds
the Comp of (Ens W) . x = the Comp of (Ens V) . x
proof
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in dom the Comp of (Ens W) or [x,y] in dom the Comp of (Ens V) )
assume A5: [x,y] in dom the Comp of (Ens W) ; ::_thesis: [x,y] in dom the Comp of (Ens V)
then consider m2, m1 being Element of Maps W such that
A6: [x,y] = [m2,m1] by A3, DOMAIN_1:1;
reconsider m19 = m1, m29 = m2 as Element of Maps V by Th7, TARSKI:def_3;
A7: ( dom m29 = dom m2 & cod m19 = cod m1 ) ;
 dom m2 = cod m1 by A5, A6, Def11;
hence  [x,y] in dom the Comp of (Ens V) by A6, A7, Def11; ::_thesis: verum
end;
let x be set ; ::_thesis: ( x in dom the Comp of (Ens W) implies the Comp of (Ens W) . x = the Comp of (Ens V) . x )
assume A8: x in dom the Comp of (Ens W) ; ::_thesis: the Comp of (Ens W) . x = the Comp of (Ens V) . x
then consider m2, m1 being Element of Maps W such that
A9: x = [m2,m1] by A3, DOMAIN_1:1;
reconsider m19 = m1, m29 = m2 as Element of Maps V by Th7, TARSKI:def_3;
A10: dom m29 = cod m19 by A4, A8, A9, Def11;
A11: dom m2 = cod m1 by A8, A9, Def11;
then A12: m2 * m1 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] by Def6;
 ( dom m1 = dom m19 & cod m2 = cod m29 ) ;
then  m29 * m19 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] by A10, Def6;
hence  the Comp of (Ens W) . x = m29 * m19 by A9, A11, A12, Def11
.= the Comp of (Ens V) . x by A9, A10, Def11 ;
::_thesis: verum
end;
hence  the Comp of (Ens W) c= the Comp of (Ens V) by GRFUNC_1:2; ::_thesis: for b1 being Element of the carrier of (Ens W)
for b2 being Element of the carrier of (Ens V) holds
( not b1 = b2 or id b1 = id b2 )
let a be Object of (Ens W); ::_thesis: for b1 being Element of the carrier of (Ens V) holds
( not a = b1 or id a = id b1 )
let a9 be Object of (Ens V); ::_thesis: ( not a = a9 or id a = id a9 )
A13: id$ (@ a) = [[(@ a),(@ a)],(id (@ a))] ;
assume  a = a9 ; ::_thesis: id a = id a9
hence  id a = id$ (@ a9) by A13, Th29
.= id a9 by Th29 ;
::_thesis: verum
end;

theorem :: ENS_1:40
for V being non empty set
for W being non empty Subset of V holds Ens W is full Subcategory of Ens V
proof
let V be non empty set ; ::_thesis: for W being non empty Subset of V holds Ens W is full Subcategory of Ens V
let W be non empty Subset of V; ::_thesis: Ens W is full Subcategory of Ens V
reconsider E = Ens W as Subcategory of Ens V by Lm7;
 for a, b being Object of E
for a9, b9 being Object of (Ens V) st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
proof
let a, b be Object of E; ::_thesis: for a9, b9 being Object of (Ens V) st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
let a9, b9 be Object of (Ens V); ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )
assume A1: ( a = a9 & b = b9 ) ; ::_thesis: Hom (a,b) = Hom (a9,b9)
reconsider aa = a, bb = b as Element of (Ens W) ;
 ( Hom (aa,bb) = Maps ((@ aa),(@ bb)) & Hom (a9,b9) = Maps ((@ a9),(@ b9)) ) by Th27;
hence  Hom (a,b) = Hom (a9,b9) by A1, Lm5; ::_thesis: verum
end;
hence  Ens W is full Subcategory of Ens V by CAT_2:def_6; ::_thesis: verum
end;

begin


definition
let C be Category;
func Hom C ->  set  equals :: ENS_1:def 18
 {  (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_18_:_
 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
set a = the Object of C;
 Hom ( the Object of C, the Object of C) in  {  (Hom (a9,b9)) where a9, b9 is Object of C : verum  }  ;
hence  not Hom C is empty ; ::_thesis: verum
end;
end;

theorem :: ENS_1:41
for C being Category
for a, b being Object of C holds Hom (a,b) in Hom C ;

theorem :: ENS_1:42
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
let C be Category; ::_thesis: 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) = {} ) )
let a be Object of C; ::_thesis: 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) = {} ) )
let f be Morphism of C; ::_thesis: ( ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) & ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) )
 Hom ((dom f),(cod f)) <> {} by CAT_1:2;
hence  ( ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) & ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) ) by CAT_1:24; ::_thesis: verum
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 :Def19: :: ENS_1:def 19
 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
defpred S1[ set , set ] means  for g being Morphism of C st g = $1 holds
$2 = f (*) g;
set X = Hom (a,(dom f));
set Y = Hom (a,(cod f));
A1: for x being set st x in Hom (a,(dom f)) holds
ex y being set st
( y in Hom (a,(cod f)) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in Hom (a,(dom f)) implies ex y being set st
( y in Hom (a,(cod f)) & S1[x,y] ) )
assume A2: x in Hom (a,(dom f)) ; ::_thesis: ex y being set st
( y in Hom (a,(cod f)) & S1[x,y] )
then reconsider g = x as Morphism of a, dom f by CAT_1:def_5;
take  f (*) g ; ::_thesis: ( f (*) g in Hom (a,(cod f)) & S1[x,f (*) g] )
 ( Hom ((dom f),(cod f)) <> {} & f is Morphism of dom f, cod f ) by CAT_1:1, CAT_1:4;
hence  ( f (*) g in Hom (a,(cod f)) & S1[x,f (*) g] ) by A2, CAT_1:23; ::_thesis: verum
end;
consider h being Function such that
A3: ( dom h = Hom (a,(dom f)) & rng h c= Hom (a,(cod f)) ) and
A4: for x being set st x in Hom (a,(dom f)) holds
S1[x,h . x] from FUNCT_1:sch_5(A1);
 Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then  ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) by CAT_1:24;
then reconsider h = h as Function of (Hom (a,(dom f))),(Hom (a,(cod f))) by A3, FUNCT_2:def_1, RELSET_1:4;
take  h ; ::_thesis: for g being Morphism of C st g in Hom (a,(dom f)) holds
h . g = f (*) g
thus  for g being Morphism of C st g in Hom (a,(dom f)) holds
h . g = f (*) g by A4; ::_thesis: verum
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
set X = Hom (a,(dom f));
set Y = Hom (a,(cod f));
let h1, h2 be Function of (Hom (a,(dom f))),(Hom (a,(cod f))); ::_thesis: ( ( for g being Morphism of C st g in Hom (a,(dom f)) holds
h1 . g = f (*) g ) & ( for g being Morphism of C st g in Hom (a,(dom f)) holds
h2 . g = f (*) g ) implies h1 = h2 )
assume that
A5: for g being Morphism of C st g in Hom (a,(dom f)) holds
h1 . g = f (*) g and
A6: for g being Morphism of C st g in Hom (a,(dom f)) holds
h2 . g = f (*) g ; ::_thesis: h1 = h2
now__::_thesis:_for_x_being_set_st_x_in_Hom_(a,(dom_f))_holds_
h1_._x_=_h2_._x
let x be set ; ::_thesis: ( x in Hom (a,(dom f)) implies h1 . x = h2 . x )
assume A7: x in Hom (a,(dom f)) ; ::_thesis: h1 . x = h2 . x
then reconsider g = x as Morphism of C ;
thus h1 . x = f (*) g by A5, A7
.= h2 . x by A6, A7 ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:12; ::_thesis: verum
end;
func hom (f,a) ->  Function of (Hom ((cod f),a)),(Hom ((dom f),a)) means :Def20: :: ENS_1:def 20
 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
defpred S1[ set , set ] means  for g being Morphism of C st g = $1 holds
$2 = g (*) f;
set X = Hom ((cod f),a);
set Y = Hom ((dom f),a);
A8: for x being set st x in Hom ((cod f),a) holds
ex y being set st
( y in Hom ((dom f),a) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in Hom ((cod f),a) implies ex y being set st
( y in Hom ((dom f),a) & S1[x,y] ) )
assume A9: x in Hom ((cod f),a) ; ::_thesis: ex y being set st
( y in Hom ((dom f),a) & S1[x,y] )
then reconsider g = x as Morphism of cod f,a by CAT_1:def_5;
take  g (*) f ; ::_thesis: ( g (*) f in Hom ((dom f),a) & S1[x,g (*) f] )
 ( Hom ((dom f),(cod f)) <> {} & f is Morphism of dom f, cod f ) by CAT_1:2, CAT_1:4;
hence  ( g (*) f in Hom ((dom f),a) & S1[x,g (*) f] ) by A9, CAT_1:23; ::_thesis: verum
end;
consider h being Function such that
A10: ( dom h = Hom ((cod f),a) & rng h c= Hom ((dom f),a) ) and
A11: for x being set st x in Hom ((cod f),a) holds
S1[x,h . x] from FUNCT_1:sch_5(A8);
 Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then  ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) by CAT_1:24;
then reconsider h = h as Function of (Hom ((cod f),a)),(Hom ((dom f),a)) by A10, FUNCT_2:def_1, RELSET_1:4;
take  h ; ::_thesis: for g being Morphism of C st g in Hom ((cod f),a) holds
h . g = g (*) f
thus  for g being Morphism of C st g in Hom ((cod f),a) holds
h . g = g (*) f by A11; ::_thesis: verum
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
set X = Hom ((cod f),a);
set Y = Hom ((dom f),a);
let h1, h2 be Function of (Hom ((cod f),a)),(Hom ((dom f),a)); ::_thesis: ( ( for g being Morphism of C st g in Hom ((cod f),a) holds
h1 . g = g (*) f ) & ( for g being Morphism of C st g in Hom ((cod f),a) holds
h2 . g = g (*) f ) implies h1 = h2 )
assume that
A12: for g being Morphism of C st g in Hom ((cod f),a) holds
h1 . g = g (*) f and
A13: for g being Morphism of C st g in Hom ((cod f),a) holds
h2 . g = g (*) f ; ::_thesis: h1 = h2
now__::_thesis:_for_x_being_set_st_x_in_Hom_((cod_f),a)_holds_
h1_._x_=_h2_._x
let x be set ; ::_thesis: ( x in Hom ((cod f),a) implies h1 . x = h2 . x )
assume A14: x in Hom ((cod f),a) ; ::_thesis: h1 . x = h2 . x
then reconsider g = x as Morphism of C ;
thus h1 . x = g (*) f by A12, A14
.= h2 . x by A13, A14 ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def19 defines hom ENS_1:def_19_:_
 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 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 ((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
for C being Category
for a, c being Object of C holds hom (a,(id c)) = id (Hom (a,c))
proof
let C be Category; ::_thesis: for a, c being Object of C holds hom (a,(id c)) = id (Hom (a,c))
let a, c be Object of C; ::_thesis: hom (a,(id c)) = id (Hom (a,c))
set A = Hom (a,c);
now__::_thesis:_(_dom_(hom_(a,(id_c)))_=_Hom_(a,c)_&_(_for_x_being_set_st_x_in_Hom_(a,c)_holds_
(hom_(a,(id_c)))_._x_=_x_)_)
 ( Hom (a,c) = {} implies Hom (a,c) = {} ) ;
hence  dom (hom (a,(id c))) = Hom (a,c) by FUNCT_2:def_1; ::_thesis: for x being set st x in Hom (a,c) holds
(hom (a,(id c))) . x = x
let x be set ; ::_thesis: ( x in Hom (a,c) implies (hom (a,(id c))) . x = x )
assume A1: x in Hom (a,c) ; ::_thesis: (hom (a,(id c))) . x = x
then reconsider g = x as Morphism of C ;
A2: cod g = c by A1, CAT_1:1;
thus (hom (a,(id c))) . x = (id c) (*) g by A1, Def19
.= x by A2, CAT_1:21 ; ::_thesis: verum
end;
hence  hom (a,(id c)) = id (Hom (a,c)) by FUNCT_1:17; ::_thesis: verum
end;

theorem Th44: :: ENS_1:44
for C being Category
for c, a being Object of C holds hom ((id c),a) = id (Hom (c,a))
proof
let C be Category; ::_thesis: for c, a being Object of C holds hom ((id c),a) = id (Hom (c,a))
let c, a be Object of C; ::_thesis: hom ((id c),a) = id (Hom (c,a))
set A = Hom (c,a);
now__::_thesis:_(_dom_(hom_((id_c),a))_=_Hom_(c,a)_&_(_for_x_being_set_st_x_in_Hom_(c,a)_holds_
(hom_((id_c),a))_._x_=_x_)_)
 ( Hom (c,a) = {} implies Hom (c,a) = {} ) ;
hence  dom (hom ((id c),a)) = Hom (c,a) by FUNCT_2:def_1; ::_thesis: for x being set st x in Hom (c,a) holds
(hom ((id c),a)) . x = x
let x be set ; ::_thesis: ( x in Hom (c,a) implies (hom ((id c),a)) . x = x )
assume A1: x in Hom (c,a) ; ::_thesis: (hom ((id c),a)) . x = x
then reconsider g = x as Morphism of C ;
A2: dom g = c by A1, CAT_1:1;
thus (hom ((id c),a)) . x = g (*) (id c) by A1, Def20
.= x by A2, CAT_1:22 ; ::_thesis: verum
end;
hence  hom ((id c),a) = id (Hom (c,a)) by FUNCT_1:17; ::_thesis: verum
end;

theorem Th45: :: ENS_1:45
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
let C be Category; ::_thesis: 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))
let a be Object of C; ::_thesis: for g, f being Morphism of C st dom g = cod f holds
hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))
let g, f be Morphism of C; ::_thesis: ( dom g = cod f implies hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f)) )
assume A1: dom g = cod f ; ::_thesis: hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))
then A2: dom (g (*) f) = dom f by CAT_1:17;
A3: cod (g (*) f) = cod g by A1, CAT_1:17;
now__::_thesis:_(_dom_(hom_(a,(g_(*)_f)))_=_Hom_(a,(dom_f))_&_dom_((hom_(a,g))_*_(hom_(a,f)))_=_Hom_(a,(dom_f))_&_(_for_x_being_set_st_x_in_Hom_(a,(dom_f))_holds_
(hom_(a,(g_(*)_f)))_._x_=_((hom_(a,g))_*_(hom_(a,f)))_._x_)_)
set h = hom (a,(g (*) f));
set h2 = hom (a,g);
set h1 = hom (a,f);
A4: Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then A5: ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) by CAT_1:24;
 Hom ((dom g),(cod g)) <> {} by CAT_1:2;
then A6: ( Hom (a,(cod g)) = {} implies Hom (a,(dom g)) = {} ) by CAT_1:24;
hence  dom (hom (a,(g (*) f))) = Hom (a,(dom f)) by A1, A2, A3, A5, FUNCT_2:def_1; ::_thesis: ( dom ((hom (a,g)) * (hom (a,f))) = Hom (a,(dom f)) & ( for x being set st x in Hom (a,(dom f)) holds
(hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x ) )
thus A7: dom ((hom (a,g)) * (hom (a,f))) = Hom (a,(dom f)) by A1, A5, A6, FUNCT_2:def_1; ::_thesis: for x being set st x in Hom (a,(dom f)) holds
(hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x
let x be set ; ::_thesis: ( x in Hom (a,(dom f)) implies (hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x )
assume A8: x in Hom (a,(dom f)) ; ::_thesis: (hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x
then reconsider f9 = x as Morphism of C ;
A9: cod f9 = dom f by A8, CAT_1:1;
A10: (hom (a,f)) . x in Hom (a,(dom g)) by A1, A4, A8, CAT_1:24, FUNCT_2:5;
then reconsider g9 = (hom (a,f)) . x as Morphism of C ;
thus (hom (a,(g (*) f))) . x = (g (*) f) (*) f9 by A2, A8, Def19
.= g (*) (f (*) f9) by A1, A9, CAT_1:18
.= g (*) g9 by A8, Def19
.= (hom (a,g)) . g9 by A10, Def19
.= ((hom (a,g)) * (hom (a,f))) . x by A7, A8, FUNCT_1:12 ; ::_thesis: verum
end;
hence  hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f)) by FUNCT_1:2; ::_thesis: verum
end;

theorem Th46: :: ENS_1:46
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
let C be Category; ::_thesis: 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))
let a be Object of C; ::_thesis: for g, f being Morphism of C st dom g = cod f holds
hom ((g (*) f),a) = (hom (f,a)) * (hom (g,a))
let g, f be Morphism of C; ::_thesis: ( dom g = cod f implies hom ((g (*) f),a) = (hom (f,a)) * (hom (g,a)) )
assume A1: dom g = cod f ; ::_thesis: hom ((g (*) f),a) = (hom (f,a)) * (hom (g,a))
then A2: cod (g (*) f) = cod g by CAT_1:17;
A3: dom (g (*) f) = dom f by A1, CAT_1:17;
now__::_thesis:_(_dom_(hom_((g_(*)_f),a))_=_Hom_((cod_g),a)_&_dom_((hom_(f,a))_*_(hom_(g,a)))_=_Hom_((cod_g),a)_&_(_for_x_being_set_st_x_in_Hom_((cod_g),a)_holds_
(hom_((g_(*)_f),a))_._x_=_((hom_(f,a))_*_(hom_(g,a)))_._x_)_)
set h = hom ((g (*) f),a);
set h2 = hom (g,a);
set h1 = hom (f,a);
A4: Hom ((dom g),(cod g)) <> {} by CAT_1:2;
then A5: ( Hom ((dom g),a) = {} implies Hom ((cod g),a) = {} ) by CAT_1:24;
 Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then A6: ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) by CAT_1:24;
hence  dom (hom ((g (*) f),a)) = Hom ((cod g),a) by A1, A3, A2, A5, FUNCT_2:def_1; ::_thesis: ( dom ((hom (f,a)) * (hom (g,a))) = Hom ((cod g),a) & ( for x being set st x in Hom ((cod g),a) holds
(hom ((g (*) f),a)) . x = ((hom (f,a)) * (hom (g,a))) . x ) )
thus A7: dom ((hom (f,a)) * (hom (g,a))) = Hom ((cod g),a) by A1, A6, A5, FUNCT_2:def_1; ::_thesis: for x being set st x in Hom ((cod g),a) holds
(hom ((g (*) f),a)) . x = ((hom (f,a)) * (hom (g,a))) . x
let x be set ; ::_thesis: ( x in Hom ((cod g),a) implies (hom ((g (*) f),a)) . x = ((hom (f,a)) * (hom (g,a))) . x )
assume A8: x in Hom ((cod g),a) ; ::_thesis: (hom ((g (*) f),a)) . x = ((hom (f,a)) * (hom (g,a))) . x
then reconsider f9 = x as Morphism of C ;
A9: dom f9 = cod g by A8, CAT_1:1;
A10: (hom (g,a)) . x in Hom ((cod f),a) by A1, A4, A8, CAT_1:24, FUNCT_2:5;
then reconsider g9 = (hom (g,a)) . x as Morphism of C ;
thus (hom ((g (*) f),a)) . x = f9 (*) (g (*) f) by A2, A8, Def20
.= (f9 (*) g) (*) f by A1, A9, CAT_1:18
.= g9 (*) f by A8, Def20
.= (hom (f,a)) . g9 by A10, Def20
.= ((hom (f,a)) * (hom (g,a))) . x by A7, A8, FUNCT_1:12 ; ::_thesis: verum
end;
hence  hom ((g (*) f),a) = (hom (f,a)) * (hom (g,a)) by FUNCT_1:2; ::_thesis: verum
end;

theorem Th47: :: ENS_1:47
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
let C be Category; ::_thesis: 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)
let a be Object of C; ::_thesis: for f being Morphism of C holds [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] is Element of Maps (Hom C)
let f be Morphism of C; ::_thesis: [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] is Element of Maps (Hom C)
 Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then A1: ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) by CAT_1:24;
 ( Hom (a,(dom f)) in Hom C & Hom (a,(cod f)) in Hom C ) ;
hence  [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] is Element of Maps (Hom C) by A1, Th5; ::_thesis: verum
end;

theorem Th48: :: ENS_1:48
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
let C be Category; ::_thesis: 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)
let a be Object of C; ::_thesis: for f being Morphism of C holds [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] is Element of Maps (Hom C)
let f be Morphism of C; ::_thesis: [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] is Element of Maps (Hom C)
 Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then A1: ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) by CAT_1:24;
 ( Hom ((dom f),a) in Hom C & Hom ((cod f),a) in Hom C ) ;
hence  [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] is Element of Maps (Hom C) by A1, Th5; ::_thesis: verum
end;

definition
let C be Category;
let a be Object of C;
func hom?- a ->  Function of the carrier' of C,(Maps (Hom C)) means :Def21: :: ENS_1:def 21
 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 carrier' 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
defpred S1[ set , set ] means  for f being Morphism of C st f = $1 holds
$2 = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))];
set X = the carrier' of C;
set Y = Maps (Hom C);
A1: for x being set st x in the carrier' of C holds
ex y being set st
( y in Maps (Hom C) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier' of C implies ex y being set st
( y in Maps (Hom C) & S1[x,y] ) )
assume  x in the carrier' of C ; ::_thesis: ex y being set st
( y in Maps (Hom C) & S1[x,y] )
then reconsider f = x as Morphism of C ;
take y = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]; ::_thesis: ( y in Maps (Hom C) & S1[x,y] )
 y is Element of Maps (Hom C) by Th47;
hence  ( y in Maps (Hom C) & S1[x,y] ) ; ::_thesis: verum
end;
consider h being Function such that
A2: ( dom h = the carrier' of C & rng h c= Maps (Hom C) ) and
A3: for x being set st x in the carrier' of C holds
S1[x,h . x] from FUNCT_1:sch_5(A1);
reconsider h = h as Function of the carrier' of C,(Maps (Hom C)) by A2, FUNCT_2:def_1, RELSET_1:4;
take  h ; ::_thesis: for f being Morphism of C holds h . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]
thus  for f being Morphism of C holds h . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of the carrier' 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
let h1, h2 be Function of the carrier' of C,(Maps (Hom C)); ::_thesis: ( ( for f being Morphism of C holds h1 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ) & ( for f being Morphism of C holds h2 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ) implies h1 = h2 )
assume that
A4: for f being Morphism of C holds h1 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] and
A5: for f being Morphism of C holds h2 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ; ::_thesis: h1 = h2
now__::_thesis:_for_f_being_Morphism_of_C_holds_h1_._f_=_h2_._f
let f be Morphism of C; ::_thesis: h1 . f = h2 . f
thus h1 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] by A4
.= h2 . f by A5 ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:63; ::_thesis: verum
end;
func hom-? a ->  Function of the carrier' of C,(Maps (Hom C)) means :Def22: :: ENS_1:def 22
 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 carrier' 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
defpred S1[ set , set ] means  for f being Morphism of C st f = $1 holds
$2 = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))];
set X = the carrier' of C;
set Y = Maps (Hom C);
A6: for x being set st x in the carrier' of C holds
ex y being set st
( y in Maps (Hom C) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier' of C implies ex y being set st
( y in Maps (Hom C) & S1[x,y] ) )
assume  x in the carrier' of C ; ::_thesis: ex y being set st
( y in Maps (Hom C) & S1[x,y] )
then reconsider f = x as Morphism of C ;
take y = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]; ::_thesis: ( y in Maps (Hom C) & S1[x,y] )
 y is Element of Maps (Hom C) by Th48;
hence  ( y in Maps (Hom C) & S1[x,y] ) ; ::_thesis: verum
end;
consider h being Function such that
A7: ( dom h = the carrier' of C & rng h c= Maps (Hom C) ) and
A8: for x being set st x in the carrier' of C holds
S1[x,h . x] from FUNCT_1:sch_5(A6);
reconsider h = h as Function of the carrier' of C,(Maps (Hom C)) by A7, FUNCT_2:def_1, RELSET_1:4;
take  h ; ::_thesis: for f being Morphism of C holds h . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]
thus  for f being Morphism of C holds h . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] by A8; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of the carrier' 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
let h1, h2 be Function of the carrier' of C,(Maps (Hom C)); ::_thesis: ( ( for f being Morphism of C holds h1 . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] ) & ( for f being Morphism of C holds h2 . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] ) implies h1 = h2 )
assume that
A9: for f being Morphism of C holds h1 . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] and
A10: for f being Morphism of C holds h2 . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] ; ::_thesis: h1 = h2
now__::_thesis:_for_f_being_Morphism_of_C_holds_h1_._f_=_h2_._f
let f be Morphism of C; ::_thesis: h1 . f = h2 . f
thus h1 . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] by A9
.= h2 . f by A10 ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def21 defines hom?- ENS_1:def_21_:_
 for C being Category
for a being Object of C
for b3 being Function of the carrier' 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 Def22 defines hom-? ENS_1:def_22_:_
 for C being Category
for a being Object of C
for b3 being Function of the carrier' 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))] );

Lm8:  for V being non empty set
for C being Category
for T being Function of the carrier' of C,(Maps (Hom C)) st Hom C c= V holds
T is Function of the carrier' of C, the carrier' of (Ens V)
proof
let V be non empty set ; ::_thesis: for C being Category
for T being Function of the carrier' of C,(Maps (Hom C)) st Hom C c= V holds
T is Function of the carrier' of C, the carrier' of (Ens V)
let C be Category; ::_thesis: for T being Function of the carrier' of C,(Maps (Hom C)) st Hom C c= V holds
T is Function of the carrier' of C, the carrier' of (Ens V)
let T be Function of the carrier' of C,(Maps (Hom C)); ::_thesis: ( Hom C c= V implies T is Function of the carrier' of C, the carrier' of (Ens V) )
assume  Hom C c= V ; ::_thesis: T is Function of the carrier' of C, the carrier' of (Ens V)
then  Maps (Hom C) c= Maps V by Th7;
hence  T is Function of the carrier' of C, the carrier' of (Ens V) by FUNCT_2:7; ::_thesis: verum
end;

Lm9:  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
let V be non empty set ; ::_thesis: 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
let C be Category; ::_thesis: 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
let a, c be Object of C; ::_thesis: ( Hom C c= V implies for d being Object of (Ens V) st d = Hom (a,c) holds
(hom?- a) . (id c) = id d )
A1: Hom (a,c) in Hom C ;
assume  Hom C c= V ; ::_thesis: for d being Object of (Ens V) st d = Hom (a,c) holds
(hom?- a) . (id c) = id d
then reconsider A = Hom (a,c) as Element of V by A1;
A2: hom (a,(id c)) = id A by Th43;
let d be Object of (Ens V); ::_thesis: ( d = Hom (a,c) implies (hom?- a) . (id c) = id d )
assume  d = Hom (a,c) ; ::_thesis: (hom?- a) . (id c) = id d
hence (hom?- a) . (id c) = id$ (@ d) by A2, Def21
.= id d by Th29 ;
::_thesis: verum
end;

Lm10:  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
let V be non empty set ; ::_thesis: 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
let C be Category; ::_thesis: 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
let c, a be Object of C; ::_thesis: ( Hom C c= V implies for d being Object of (Ens V) st d = Hom (c,a) holds
(hom-? a) . (id c) = id d )
A1: Hom (c,a) in Hom C ;
assume  Hom C c= V ; ::_thesis: for d being Object of (Ens V) st d = Hom (c,a) holds
(hom-? a) . (id c) = id d
then reconsider A = Hom (c,a) as Element of V by A1;
A2: hom ((id c),a) = id A by Th44;
let d be Object of (Ens V); ::_thesis: ( d = Hom (c,a) implies (hom-? a) . (id c) = id d )
assume  d = Hom (c,a) ; ::_thesis: (hom-? a) . (id c) = id d
hence (hom-? a) . (id c) = id$ (@ d) by A2, Def22
.= id d by Th29 ;
::_thesis: verum
end;

theorem Th49: :: ENS_1:49
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
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 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 Functor of C, Ens V
let a be Object of C; ::_thesis: ( Hom C c= V implies hom?- a is Functor of C, Ens V )
assume A1: Hom C c= V ; ::_thesis: hom?- a is 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_(dom_(T_._f))_&_T_._(id_(cod_f))_=_id_(cod_(T_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_
T_._(g_(*)_f)_=_(T_._g)_(*)_(T_._f)_)_)
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 (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )
proof
let c be Object of C; ::_thesis: ex d being Object of (Ens V) st T . (id c) = id d
 Hom (a,c) in Hom C ;
then reconsider A = Hom (a,c) 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 (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f)
proof
let f be Morphism of C; ::_thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
set b = dom f;
set c = cod f;
set g = T . f;
 ( Hom (a,(dom f)) in Hom C & Hom (a,(cod f)) in Hom C ) ;
then reconsider A = Hom (a,(dom f)), B = Hom (a,(cod f)) as Element of V by A1;
A2: [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] = @ (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 (@ A) by A1, Lm9
.= id (dom (T . f)) by A2, Lm1 ; ::_thesis: T . (id (cod f)) = id (cod (T . f))
thus T . (id (cod f)) = id (@ B) by A1, Lm9
.= id (cod (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 . g) (*) (T . f) )
assume A3: dom g = cod f ; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f)
A4: [[(Hom (a,(dom g))),(Hom (a,(cod g)))],(hom (a,g))] = @ (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 (a,g) by XTUPLE_0:1;
 cod (T . g) = Hom (a,(cod g)) by A4, Lm1;
then A6: cod (@ (T . g)) = Hom (a,(cod g)) by Def10;
A7: dom (T . g) = Hom (a,(dom g)) by A4, Lm1;
then A8: dom (@ (T . g)) = Hom (a,(dom g)) by Def9;
A9: [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] = @ (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 (a,f) by XTUPLE_0:1;
 dom (T . f) = Hom (a,(dom f)) by A9, Lm1;
then A11: dom (@ (T . f)) = Hom (a,(dom f)) by Def9;
A12: cod (T . f) = Hom (a,(cod f)) by A9, Lm1;
then A13: cod (@ (T . f)) = Hom (a,(cod f)) by Def10;
 ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A3, CAT_1:17;
hence T . (g (*) f) = [[(Hom (a,(dom f))),(Hom (a,(cod g)))],(hom (a,(g (*) f)))] by Def21
.= [[(Hom (a,(dom f))),(Hom (a,(cod g)))],((hom (a,g)) * (hom (a,f)))] by A3, Th45
.= (@ (T . g)) * (@ (T . f)) by A3, A10, A11, A13, A5, A8, A6, Def6
.= (T . g) (*) (T . f) by A3, A12, A7, Th28 ;
::_thesis: verum
end;
hence  hom?- a is Functor of C, Ens V by CAT_1:61; ::_thesis: verum
end;

theorem Th50: :: ENS_1:50
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
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;
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)_)_)
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, Lm10; ::_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;
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 Def22
.= [[(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;
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)
A4: [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] = @ (T . g) by Def22
.= [[(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 Def22
.= [[(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 Def22
.= [[(Hom ((cod g),a)),(Hom ((dom f),a))],((hom (f,a)) * (hom (g,a)))] by A3, Th46
.= (@ (T . f)) * (@ (T . g)) by A3, A10, A13, A11, A5, A6, A8, Def6
.= (T . f) (*) (T . g) by A3, A12, A7, Th28 ;
::_thesis: verum
end;
hence  hom-? a is Contravariant_Functor of C, Ens V by OPPCAT_1:def_9; ::_thesis: verum
end;

theorem Th51: :: ENS_1:51
for C being Category
for f, f9 being Morphism of C st Hom ((dom f),(cod f9)) = {} holds
Hom ((cod f),(dom f9)) = {}
proof
let C be Category; ::_thesis: for f, f9 being Morphism of C st Hom ((dom f),(cod f9)) = {} holds
Hom ((cod f),(dom f9)) = {}
let f, f9 be Morphism of C; ::_thesis: ( Hom ((dom f),(cod f9)) = {} implies Hom ((cod f),(dom f9)) = {} )
assume that
A1: Hom ((dom f),(cod f9)) = {} and
A2: Hom ((cod f),(dom f9)) <> {} ; ::_thesis: contradiction
A3: Hom ((dom f9),(cod f9)) <> {} by CAT_1:2;
 Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then  Hom ((dom f),(dom f9)) <> {} by A2, CAT_1:24;
hence  contradiction by A1, A3, CAT_1:24; ::_thesis: verum
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 :Def23: :: ENS_1:def 23
 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
defpred S1[ set , set ] means  for h being Morphism of C st h = $1 holds
$2 = (g (*) h) (*) f;
set X = Hom ((cod f),(dom g));
set Y = Hom ((dom f),(cod g));
A1: for x being set st x in Hom ((cod f),(dom g)) holds
ex y being set st
( y in Hom ((dom f),(cod g)) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in Hom ((cod f),(dom g)) implies ex y being set st
( y in Hom ((dom f),(cod g)) & S1[x,y] ) )
A2: ( Hom ((dom f),(cod f)) <> {} & f is Morphism of dom f, cod f ) by CAT_1:2, CAT_1:4;
assume A3: x in Hom ((cod f),(dom g)) ; ::_thesis: ex y being set st
( y in Hom ((dom f),(cod g)) & S1[x,y] )
then reconsider h = x as Morphism of cod f, dom g by CAT_1:def_5;
take  (g (*) h) (*) f ; ::_thesis: ( (g (*) h) (*) f in Hom ((dom f),(cod g)) & S1[x,(g (*) h) (*) f] )
 ( Hom ((dom g),(cod g)) <> {} & g is Morphism of dom g, cod g ) by CAT_1:2, CAT_1:4;
then A4: g (*) h in Hom ((cod f),(cod g)) by A3, CAT_1:23;
then  g (*) h is Morphism of cod f, cod g by CAT_1:def_5;
hence  ( (g (*) h) (*) f in Hom ((dom f),(cod g)) & S1[x,(g (*) h) (*) f] ) by A4, A2, CAT_1:23; ::_thesis: verum
end;
consider h being Function such that
A5: ( dom h = Hom ((cod f),(dom g)) & rng h c= Hom ((dom f),(cod g)) ) and
A6: for x being set st x in Hom ((cod f),(dom g)) holds
S1[x,h . x] from FUNCT_1:sch_5(A1);
 ( Hom ((dom f),(cod g)) = {} implies Hom ((cod f),(dom g)) = {} ) by Th51;
then reconsider h = h as Function of (Hom ((cod f),(dom g))),(Hom ((dom f),(cod g))) by A5, FUNCT_2:def_1, RELSET_1:4;
take  h ; ::_thesis: for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
h . h = (g (*) h) (*) f
thus  for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
h . h = (g (*) h) (*) f by A6; ::_thesis: verum
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
set X = Hom ((cod f),(dom g));
set Y = Hom ((dom f),(cod g));
let h1, h2 be Function of (Hom ((cod f),(dom g))),(Hom ((dom f),(cod g))); ::_thesis: ( ( for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
h1 . h = (g (*) h) (*) f ) & ( for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
h2 . h = (g (*) h) (*) f ) implies h1 = h2 )
assume that
A7: for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
h1 . h = (g (*) h) (*) f and
A8: for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
h2 . h = (g (*) h) (*) f ; ::_thesis: h1 = h2
now__::_thesis:_for_x_being_set_st_x_in_Hom_((cod_f),(dom_g))_holds_
h1_._x_=_h2_._x
let x be set ; ::_thesis: ( x in Hom ((cod f),(dom g)) implies h1 . x = h2 . x )
assume A9: x in Hom ((cod f),(dom g)) ; ::_thesis: h1 . x = h2 . x
then reconsider h = x as Morphism of C ;
thus h1 . x = (g (*) h) (*) f by A7, A9
.= h2 . x by A8, A9 ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def23 defines hom ENS_1:def_23_:_
 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
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
let C be Category; ::_thesis: 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)
let f, g be Morphism of C; ::_thesis: [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] is Element of Maps (Hom C)
A1: ( Hom ((dom f),(cod g)) in Hom C & Hom ((cod f),(dom g)) in Hom C ) ;
 ( Hom ((dom f),(cod g)) = {} implies Hom ((cod f),(dom g)) = {} ) by Th51;
hence  [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] is Element of Maps (Hom C) by A1, Th5; ::_thesis: verum
end;

theorem Th53: :: ENS_1:53
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
let C be Category; ::_thesis: 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) )
let a be Object of C; ::_thesis: for f being Morphism of C holds
( hom ((id a),f) = hom (a,f) & hom (f,(id a)) = hom (f,a) )
let f be Morphism of C; ::_thesis: ( hom ((id a),f) = hom (a,f) & hom (f,(id a)) = hom (f,a) )
A1: cod (id a) = a ;
now__::_thesis:_(_dom_(hom_((id_a),f))_=_Hom_(a,(dom_f))_&_dom_(hom_(a,f))_=_Hom_(a,(dom_f))_&_(_for_x_being_set_st_x_in_Hom_(a,(dom_f))_holds_
(hom_((id_a),f))_._x_=_(hom_(a,f))_._x_)_)
 Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then  ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) by CAT_1:24;
hence  ( dom (hom ((id a),f)) = Hom (a,(dom f)) & dom (hom (a,f)) = Hom (a,(dom f)) ) by FUNCT_2:def_1; ::_thesis: for x being set st x in Hom (a,(dom f)) holds
(hom ((id a),f)) . x = (hom (a,f)) . x
let x be set ; ::_thesis: ( x in Hom (a,(dom f)) implies (hom ((id a),f)) . x = (hom (a,f)) . x )
assume A2: x in Hom (a,(dom f)) ; ::_thesis: (hom ((id a),f)) . x = (hom (a,f)) . x
then reconsider g = x as Morphism of C ;
A3: dom g = a by A2, CAT_1:1;
A4: cod g = dom f by A2, CAT_1:1;
thus (hom ((id a),f)) . x = (f (*) g) (*) (id a) by A2, Def23
.= f (*) (g (*) (id a)) by A1, A3, A4, CAT_1:18
.= f (*) g by A3, CAT_1:22
.= (hom (a,f)) . x by A2, Def19 ; ::_thesis: verum
end;
hence  hom ((id a),f) = hom (a,f) by FUNCT_1:2; ::_thesis: hom (f,(id a)) = hom (f,a)
now__::_thesis:_(_dom_(hom_(f,(id_a)))_=_Hom_((cod_f),a)_&_dom_(hom_(f,a))_=_Hom_((cod_f),a)_&_(_for_x_being_set_st_x_in_Hom_((cod_f),a)_holds_
(hom_(f,(id_a)))_._x_=_(hom_(f,a))_._x_)_)
 Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then  ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) by CAT_1:24;
hence  ( dom (hom (f,(id a))) = Hom ((cod f),a) & dom (hom (f,a)) = Hom ((cod f),a) ) by FUNCT_2:def_1; ::_thesis: for x being set st x in Hom ((cod f),a) holds
(hom (f,(id a))) . x = (hom (f,a)) . x
let x be set ; ::_thesis: ( x in Hom ((cod f),a) implies (hom (f,(id a))) . x = (hom (f,a)) . x )
assume A5: x in Hom ((cod f),a) ; ::_thesis: (hom (f,(id a))) . x = (hom (f,a)) . x
then reconsider g = x as Morphism of C ;
A6: cod g = a by A5, CAT_1:1;
thus (hom (f,(id a))) . x = ((id a) (*) g) (*) f by A5, Def23
.= g (*) f by A6, CAT_1:21
.= (hom (f,a)) . x by A5, Def20 ; ::_thesis: verum
end;
hence  hom (f,(id a)) = hom (f,a) by FUNCT_1:2; ::_thesis: verum
end;

theorem Th54: :: ENS_1:54
for C being Category
for a, b being Object of C holds hom ((id a),(id b)) = id (Hom (a,b))
proof
let C be Category; ::_thesis: for a, b being Object of C holds hom ((id a),(id b)) = id (Hom (a,b))
let a, b be Object of C; ::_thesis: hom ((id a),(id b)) = id (Hom (a,b))
thus  hom ((id a),(id b)) = hom (a,(id b)) by Th53
.= id (Hom (a,b)) by Th43 ; ::_thesis: verum
end;

theorem :: ENS_1:55
for C being Category
for f, g being Morphism of C holds hom (f,g) = (hom ((dom f),g)) * (hom (f,(dom g)))
proof
let C be Category; ::_thesis: for f, g being Morphism of C holds hom (f,g) = (hom ((dom f),g)) * (hom (f,(dom g)))
let f, g be Morphism of C; ::_thesis: hom (f,g) = (hom ((dom f),g)) * (hom (f,(dom g)))
now__::_thesis:_(_dom_(hom_(f,g))_=_Hom_((cod_f),(dom_g))_&_dom_((hom_((dom_f),g))_*_(hom_(f,(dom_g))))_=_Hom_((cod_f),(dom_g))_&_(_for_x_being_set_st_x_in_Hom_((cod_f),(dom_g))_holds_
(hom_(f,g))_._x_=_((hom_((dom_f),g))_*_(hom_(f,(dom_g))))_._x_)_)
A1: ( Hom ((dom f),(cod g)) = {} implies Hom ((cod f),(dom g)) = {} ) by Th51;
hence  dom (hom (f,g)) = Hom ((cod f),(dom g)) by FUNCT_2:def_1; ::_thesis: ( dom ((hom ((dom f),g)) * (hom (f,(dom g)))) = Hom ((cod f),(dom g)) & ( for x being set st x in Hom ((cod f),(dom g)) holds
(hom (f,g)) . x = ((hom ((dom f),g)) * (hom (f,(dom g)))) . x ) )
 Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then  ( Hom ((dom f),(dom g)) = {} implies Hom ((cod f),(dom g)) = {} ) by CAT_1:24;
hence A2: dom ((hom ((dom f),g)) * (hom (f,(dom g)))) = Hom ((cod f),(dom g)) by A1, FUNCT_2:def_1; ::_thesis: for x being set st x in Hom ((cod f),(dom g)) holds
(hom (f,g)) . x = ((hom ((dom f),g)) * (hom (f,(dom g)))) . x
let x be set ; ::_thesis: ( x in Hom ((cod f),(dom g)) implies (hom (f,g)) . x = ((hom ((dom f),g)) * (hom (f,(dom g)))) . x )
assume A3: x in Hom ((cod f),(dom g)) ; ::_thesis: (hom (f,g)) . x = ((hom ((dom f),g)) * (hom (f,(dom g)))) . x
then reconsider h = x as Morphism of C ;
A4: dom h = cod f by A3, CAT_1:1;
then A5: dom (h (*) f) = dom f by CAT_1:17;
A6: cod h = dom g by A3, CAT_1:1;
then  cod (h (*) f) = dom g by A4, CAT_1:17;
then A7: h (*) f in Hom ((dom f),(dom g)) by A5;
thus (hom (f,g)) . x = (g (*) h) (*) f by A3, Def23
.= g (*) (h (*) f) by A4, A6, CAT_1:18
.= (hom ((dom f),g)) . (h (*) f) by A7, Def19
.= (hom ((dom f),g)) . ((hom (f,(dom g))) . h) by A3, Def20
.= ((hom ((dom f),g)) * (hom (f,(dom g)))) . x by A2, A3, FUNCT_1:12 ; ::_thesis: verum
end;
hence  hom (f,g) = (hom ((dom f),g)) * (hom (f,(dom g))) by FUNCT_1:2; ::_thesis: verum
end;

theorem Th56: :: ENS_1:56
for C being Category
for g, f, g9, f9 being Morphism of C st cod g = dom f & dom g9 = cod f9 holds
hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9))
proof
let C be Category; ::_thesis: for g, f, g9, f9 being Morphism of C st cod g = dom f & dom g9 = cod f9 holds
hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9))
let g, f, g9, f9 be Morphism of C; ::_thesis: ( cod g = dom f & dom g9 = cod f9 implies hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9)) )
assume that
A1: cod g = dom f and
A2: dom g9 = cod f9 ; ::_thesis: hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9))
A3: dom (g9 (*) f9) = dom f9 by A2, CAT_1:17;
A4: cod (f (*) g) = cod f by A1, CAT_1:17;
A5: ( cod (g9 (*) f9) = cod g9 & dom (f (*) g) = dom g ) by A1, A2, CAT_1:17;
now__::_thesis:_(_dom_(hom_((f_(*)_g),(g9_(*)_f9)))_=_Hom_((cod_f),(dom_f9))_&_dom_((hom_(g,g9))_*_(hom_(f,f9)))_=_Hom_((cod_f),(dom_f9))_&_(_for_x_being_set_st_x_in_Hom_((cod_f),(dom_f9))_holds_
(hom_((f_(*)_g),(g9_(*)_f9)))_._x_=_((hom_(g,g9))_*_(hom_(f,f9)))_._x_)_)
set h = hom ((f (*) g),(g9 (*) f9));
set h2 = hom (g,g9);
set h1 = hom (f,f9);
A6: ( Hom ((dom f),(cod f9)) = {} implies Hom ((cod f),(dom f9)) = {} ) by Th51;
A7: ( Hom ((dom g),(cod g9)) = {} implies Hom ((cod g),(dom g9)) = {} ) by Th51;
hence  dom (hom ((f (*) g),(g9 (*) f9))) = Hom ((cod f),(dom f9)) by A1, A2, A3, A5, A4, A6, FUNCT_2:def_1; ::_thesis: ( dom ((hom (g,g9)) * (hom (f,f9))) = Hom ((cod f),(dom f9)) & ( for x being set st x in Hom ((cod f),(dom f9)) holds
(hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . x ) )
thus A8: dom ((hom (g,g9)) * (hom (f,f9))) = Hom ((cod f),(dom f9)) by A1, A2, A7, A6, FUNCT_2:def_1; ::_thesis: for x being set st x in Hom ((cod f),(dom f9)) holds
(hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . x
let x be set ; ::_thesis: ( x in Hom ((cod f),(dom f9)) implies (hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . x )
assume A9: x in Hom ((cod f),(dom f9)) ; ::_thesis: (hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . x
then reconsider k = x as Morphism of C ;
A10: (hom (f,f9)) . x in Hom ((cod g),(dom g9)) by A1, A2, A9, Th51, FUNCT_2:5;
then reconsider l = (hom (f,f9)) . x as Morphism of C ;
A11: dom k = cod f by A9, CAT_1:1;
then A12: cod (k (*) (f (*) g)) = cod k by A4, CAT_1:17;
A13: cod k = dom f9 by A9, CAT_1:1;
then A14: dom (f9 (*) k) = dom k by CAT_1:17;
then A15: dom ((f9 (*) k) (*) f) = dom f by A11, CAT_1:17;
 cod (f9 (*) k) = cod f9 by A13, CAT_1:17;
then A16: cod ((f9 (*) k) (*) f) = cod f9 by A11, A14, CAT_1:17;
thus (hom ((f (*) g),(g9 (*) f9))) . x = ((g9 (*) f9) (*) k) (*) (f (*) g) by A3, A4, A9, Def23
.= (g9 (*) f9) (*) (k (*) (f (*) g)) by A3, A4, A13, A11, CAT_1:18
.= g9 (*) (f9 (*) (k (*) (f (*) g))) by A2, A13, A12, CAT_1:18
.= g9 (*) ((f9 (*) k) (*) (f (*) g)) by A4, A13, A11, CAT_1:18
.= g9 (*) (((f9 (*) k) (*) f) (*) g) by A1, A11, A14, CAT_1:18
.= (g9 (*) ((f9 (*) k) (*) f)) (*) g by A1, A2, A15, A16, CAT_1:18
.= (g9 (*) l) (*) g by A9, Def23
.= (hom (g,g9)) . l by A10, Def23
.= ((hom (g,g9)) * (hom (f,f9))) . x by A8, A9, FUNCT_1:12 ; ::_thesis: verum
end;
hence  hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9)) by FUNCT_1:2; ::_thesis: verum
end;

definition
let C be Category;
func hom?? C ->  Function of the carrier' of [:C,C:],(Maps (Hom C)) means :Def24: :: ENS_1:def 24
 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 carrier' 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
defpred S1[ set , set ] means  for f, g being Morphism of C st $1 = [f,g] holds
$2 = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))];
set X = the carrier' of [:C,C:];
set Y = Maps (Hom C);
A1: for x being set st x in the carrier' of [:C,C:] holds
ex y being set st
( y in Maps (Hom C) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier' of [:C,C:] implies ex y being set st
( y in Maps (Hom C) & S1[x,y] ) )
assume  x in the carrier' of [:C,C:] ; ::_thesis: ex y being set st
( y in Maps (Hom C) & S1[x,y] )
then consider f, g being Morphism of C such that
A2: x = [f,g] by DOMAIN_1:1;
take y = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]; ::_thesis: ( y in Maps (Hom C) & S1[x,y] )
 y is Element of Maps (Hom C) by Th52;
hence  y in Maps (Hom C) ; ::_thesis: S1[x,y]
let f9, g9 be Morphism of C; ::_thesis: ( x = [f9,g9] implies y = [[(Hom ((cod f9),(dom g9))),(Hom ((dom f9),(cod g9)))],(hom (f9,g9))] )
assume  x = [f9,g9] ; ::_thesis: y = [[(Hom ((cod f9),(dom g9))),(Hom ((dom f9),(cod g9)))],(hom (f9,g9))]
then  ( f9 = f & g9 = g ) by A2, XTUPLE_0:1;
hence  y = [[(Hom ((cod f9),(dom g9))),(Hom ((dom f9),(cod g9)))],(hom (f9,g9))] ; ::_thesis: verum
end;
consider h being Function such that
A3: ( dom h = the carrier' of [:C,C:] & rng h c= Maps (Hom C) ) and
A4: for x being set st x in the carrier' of [:C,C:] holds
S1[x,h . x] from FUNCT_1:sch_5(A1);
reconsider h = h as Function of the carrier' of [:C,C:],(Maps (Hom C)) by A3, FUNCT_2:def_1, RELSET_1:4;
take  h ; ::_thesis: for f, g being Morphism of C holds h . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]
thus  for f, g being Morphism of C holds h . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of the carrier' 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
let h1, h2 be Function of the carrier' of [:C,C:],(Maps (Hom C)); ::_thesis: ( ( for f, g being Morphism of C holds h1 . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] ) & ( for f, g being Morphism of C holds h2 . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] ) implies h1 = h2 )
assume that
A5: for f, g being Morphism of C holds h1 . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] and
A6: for f, g being Morphism of C holds h2 . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] ; ::_thesis: h1 = h2
now__::_thesis:_(_the_carrier'_of_[:C,C:]_=_[:_the_carrier'_of_C,_the_carrier'_of_C:]_&_(_for_f,_g_being_Morphism_of_C_holds_h1_._(f,g)_=_h2_._(f,g)_)_)
thus  the carrier' of [:C,C:] = [: the carrier' of C, the carrier' of C:] ; ::_thesis: for f, g being Morphism of C holds h1 . (f,g) = h2 . (f,g)
let f, g be Morphism of C; ::_thesis: h1 . (f,g) = h2 . (f,g)
thus h1 . (f,g) = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] by A5
.= h2 . (f,g) by A6 ; ::_thesis: verum
end;
hence  h1 = h2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def24 defines hom?? ENS_1:def_24_:_
 for C being Category
for b2 being Function of the carrier' 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
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
let C be Category; ::_thesis: for a being Object of C holds
( hom?- a = (curry (hom?? C)) . (id a) & hom-? a = (curry' (hom?? C)) . (id a) )
let a be Object of C; ::_thesis: ( hom?- a = (curry (hom?? C)) . (id a) & hom-? a = (curry' (hom?? C)) . (id a) )
reconsider T = hom?? C as Function of [: the carrier' of C, the carrier' of C:],(Maps (Hom C)) ;
now__::_thesis:_for_f_being_Morphism_of_C_holds_((curry_T)_._(id_a))_._f_=_(hom?-_a)_._f
let f be Morphism of C; ::_thesis: ((curry T) . (id a)) . f = (hom?- a) . f
thus ((curry T) . (id a)) . f = T . ((id a),f) by FUNCT_5:69
.= [[(Hom ((cod (id a)),(dom f))),(Hom ((dom (id a)),(cod f)))],(hom ((id a),f))] by Def24
.= [[(Hom ((cod (id a)),(dom f))),(Hom ((dom (id a)),(cod f)))],(hom (a,f))] by Th53
.= [[(Hom (a,(dom f))),(Hom ((dom (id a)),(cod f)))],(hom (a,f))]
.= [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]
.= (hom?- a) . f by Def21 ; ::_thesis: verum
end;
hence  hom?- a = (curry (hom?? C)) . (id a) by FUNCT_2:63; ::_thesis: hom-? a = (curry' (hom?? C)) . (id a)
now__::_thesis:_for_f_being_Morphism_of_C_holds_((curry'_T)_._(id_a))_._f_=_(hom-?_a)_._f
let f be Morphism of C; ::_thesis: ((curry' T) . (id a)) . f = (hom-? a) . f
thus ((curry' T) . (id a)) . f = T . (f,(id a)) by FUNCT_5:70
.= [[(Hom ((cod f),(dom (id a)))),(Hom ((dom f),(cod (id a))))],(hom (f,(id a)))] by Def24
.= [[(Hom ((cod f),(dom (id a)))),(Hom ((dom f),(cod (id a))))],(hom (f,a))] by Th53
.= [[(Hom ((cod f),a)),(Hom ((dom f),(cod (id a))))],(hom (f,a))]
.= [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]
.= (hom-? a) . f by Def22 ; ::_thesis: verum
end;
hence  hom-? a = (curry' (hom?? C)) . (id a) by FUNCT_2:63; ::_thesis: verum
end;

Lm11:  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
let V be non empty set ; ::_thesis: 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
let C be Category; ::_thesis: 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
let a, b be Object of C; ::_thesis: ( Hom C c= V implies for d being Object of (Ens V) st d = Hom (a,b) holds
(hom?? C) . [(id a),(id b)] = id d )
A1: Hom (a,b) in Hom C ;
assume  Hom C c= V ; ::_thesis: for d being Object of (Ens V) st d = Hom (a,b) holds
(hom?? C) . [(id a),(id b)] = id d
then reconsider A = Hom (a,b) as Element of V by A1;
A2: hom ((id a),(id b)) = id A by Th54;
let d be Object of (Ens V); ::_thesis: ( d = Hom (a,b) implies (hom?? C) . [(id a),(id b)] = id d )
assume  d = Hom (a,b) ; ::_thesis: (hom?? C) . [(id a),(id b)] = id d
hence (hom?? C) . [(id a),(id b)] = id$ (@ d) by A2, Def24
.= id d by Th29 ;
::_thesis: verum
end;

theorem Th58: :: ENS_1:58
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
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, Def24
.= [[(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, Def24
.= [[(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, Def24
.= [[(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 Def24
.= [[(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, Th56
.= (@ (T . gg)) * (@ (T . ff)) by A17, A18, A20, A11, A14, A12, A23, A26, Def6
.= (T . gg) (*) (T . ff) by A19, A13, A23, A26, Th28 ; ::_thesis: verum
end;
hence  hom?? C is Functor of [:(C opp),C:], Ens V by CAT_1:61; ::_thesis: verum
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 :Def25: :: ENS_1:def 25
 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 :Def26: :: ENS_1:def 26
 hom-? a;
coherence
 hom-? a is Contravariant_Functor of C, Ens V by A1, Th50;
end;

:: deftheorem Def25 defines hom?- ENS_1:def_25_:_
 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 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;

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 :Def27: :: ENS_1:def 27
 hom?? C;
coherence
 hom?? C is Functor of [:(C opp),C:], Ens V by A1, Th58;
end;

:: deftheorem Def27 defines hom?? ENS_1:def_27_:_
 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
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
let V be non empty set ; ::_thesis: 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))]
let C be Category; ::_thesis: 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))]
let a be Object of C; ::_thesis: 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))]
let f be Morphism of C; ::_thesis: ( Hom C c= V implies (hom?- (V,a)) . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] )
assume  Hom C c= V ; ::_thesis: (hom?- (V,a)) . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]
hence (hom?- (V,a)) . f = (hom?- a) . f by Def25
.= [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] by Def21 ;
::_thesis: verum
end;

theorem :: ENS_1:60
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
let V be non empty set ; ::_thesis: 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)
let C be Category; ::_thesis: for a, b being Object of C st Hom C c= V holds
(Obj (hom?- (V,a))) . b = Hom (a,b)
let a, b be Object of C; ::_thesis: ( Hom C c= V implies (Obj (hom?- (V,a))) . b = Hom (a,b) )
assume A1: Hom C c= V ; ::_thesis: (Obj (hom?- (V,a))) . b = Hom (a,b)
 Hom (a,b) in Hom C ;
then reconsider A = Hom (a,b) as Element of V by A1;
set d = @ A;
(hom?- (V,a)) . (id b) = (hom?- a) . (id b) by A1, Def25
.= id (@ A) by A1, Lm9 ;
hence  (Obj (hom?- (V,a))) . b = Hom (a,b) by CAT_1:67; ::_thesis: verum
end;

theorem :: ENS_1:61
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
let V be non empty set ; ::_thesis: 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))]
let C be Category; ::_thesis: 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))]
let a be Object of C; ::_thesis: 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))]
let f be Morphism of C; ::_thesis: ( Hom C c= V implies (hom-? (V,a)) . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] )
assume  Hom C c= V ; ::_thesis: (hom-? (V,a)) . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]
hence (hom-? (V,a)) . f = (hom-? a) . f by Def26
.= [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] by Def22 ;
::_thesis: verum
end;

theorem :: ENS_1:62
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
let V be non empty set ; ::_thesis: 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)
let C be Category; ::_thesis: for a, b being Object of C st Hom C c= V holds
(Obj (hom-? (V,a))) . b = Hom (b,a)
let a, b be Object of C; ::_thesis: ( Hom C c= V implies (Obj (hom-? (V,a))) . b = Hom (b,a) )
assume A1: Hom C c= V ; ::_thesis: (Obj (hom-? (V,a))) . b = Hom (b,a)
 Hom (b,a) in Hom C ;
then reconsider A = Hom (b,a) as Element of V by A1;
set d = @ A;
(hom-? (V,a)) . (id b) = (hom-? a) . (id b) by A1, Def26
.= id (@ A) by A1, Lm10 ;
hence  (Obj (hom-? (V,a))) . b = Hom (b,a) by OPPCAT_1:30; ::_thesis: verum
end;

theorem :: ENS_1:63
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
let V be non empty set ; ::_thesis: 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))]
let C be Category; ::_thesis: 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))]
let f, g be Morphism of C; ::_thesis: ( Hom C c= V implies (hom?? (V,C)) . [(f opp),g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] )
assume A1: Hom C c= V ; ::_thesis: (hom?? (V,C)) . [(f opp),g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]
thus (hom?? (V,C)) . [(f opp),g] = (hom?? C) . [f,g] by A1, Def27
.= [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] by Def24 ; ::_thesis: verum
end;

theorem :: ENS_1:64
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
let V be non empty set ; ::_thesis: 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)
let C be Category; ::_thesis: for a, b being Object of C st Hom C c= V holds
(Obj (hom?? (V,C))) . [(a opp),b] = Hom (a,b)
let a, b be Object of C; ::_thesis: ( Hom C c= V implies (Obj (hom?? (V,C))) . [(a opp),b] = Hom (a,b) )
assume A1: Hom C c= V ; ::_thesis: (Obj (hom?? (V,C))) . [(a opp),b] = Hom (a,b)
 Hom (a,b) in Hom C ;
then reconsider A = Hom (a,b) as Element of V by A1;
A2: id (a opp) = id a by OPPCAT_1:71;
set d = @ A;
(hom?? (V,C)) . (id [(a opp),b]) = (hom?? (V,C)) . [(id (a opp)),(id b)] by CAT_2:31
.= (hom?? C) . [(id a),(id b)] by A1, Def27, A2
.= id (@ A) by A1, Lm11 ;
hence  (Obj (hom?? (V,C))) . [(a opp),b] = Hom (a,b) by CAT_1:67; ::_thesis: verum
end;

theorem :: ENS_1:65
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
let V be non empty set ; ::_thesis: for C being Category
for a being Object of C st Hom C c= V holds
(hom?? (V,C)) ?- (a opp) = hom?- (V,a)
let C be Category; ::_thesis: for a being Object of C st Hom C c= V holds
(hom?? (V,C)) ?- (a opp) = hom?- (V,a)
let a be Object of C; ::_thesis: ( Hom C c= V implies (hom?? (V,C)) ?- (a opp) = hom?- (V,a) )
assume A1: Hom C c= V ; ::_thesis: (hom?? (V,C)) ?- (a opp) = hom?- (V,a)
A2: id (a opp) = id a by OPPCAT_1:71;
thus (hom?? (V,C)) ?- (a opp) = (curry (hom?? C)) . (id a) by A1, Def27, A2
.= hom?- a by Th57
.= hom?- (V,a) by A1, Def25 ; ::_thesis: verum
end;

theorem :: ENS_1:66
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
let V be non empty set ; ::_thesis: for C being Category
for a being Object of C st Hom C c= V holds
(hom?? (V,C)) -? a = hom-? (V,a)
let C be Category; ::_thesis: for a being Object of C st Hom C c= V holds
(hom?? (V,C)) -? a = hom-? (V,a)
let a be Object of C; ::_thesis: ( Hom C c= V implies (hom?? (V,C)) -? a = hom-? (V,a) )
assume A1: Hom C c= V ; ::_thesis: (hom?? (V,C)) -? a = hom-? (V,a)
hence (hom?? (V,C)) -? a = (curry' (hom?? C)) . (id a) by Def27
.= hom-? a by Th57
.= hom-? (V,a) by A1, Def26 ;
::_thesis: verum
end;