:: YONEDA_1 semantic presentation

begin


definition
let A be Category;
func EnsHom A ->  Category equals :: YONEDA_1:def 1
 Ens (Hom A);
correctness
coherence
Ens (Hom A) is Category;
;
end;

:: deftheorem  defines EnsHom YONEDA_1:def_1_:_
 for A being Category holds EnsHom A = Ens (Hom A);

theorem Th1: :: YONEDA_1:1
for A being Category
for f, g being Function
for m1, m2 being Morphism of (EnsHom A) st cod m1 = dom m2 & [[(dom m1),(cod m1)],f] = m1 & [[(dom m2),(cod m2)],g] = m2 holds
[[(dom m1),(cod m2)],(g * f)] = m2 (*) m1
proof
let A be Category; ::_thesis: for f, g being Function
for m1, m2 being Morphism of (EnsHom A) st cod m1 = dom m2 & [[(dom m1),(cod m1)],f] = m1 & [[(dom m2),(cod m2)],g] = m2 holds
[[(dom m1),(cod m2)],(g * f)] = m2 (*) m1
let f, g be Function; ::_thesis: for m1, m2 being Morphism of (EnsHom A) st cod m1 = dom m2 & [[(dom m1),(cod m1)],f] = m1 & [[(dom m2),(cod m2)],g] = m2 holds
[[(dom m1),(cod m2)],(g * f)] = m2 (*) m1
let m1, m2 be Morphism of (EnsHom A); ::_thesis: ( cod m1 = dom m2 & [[(dom m1),(cod m1)],f] = m1 & [[(dom m2),(cod m2)],g] = m2 implies [[(dom m1),(cod m2)],(g * f)] = m2 (*) m1 )
assume that
A1: cod m1 = dom m2 and
A2: [[(dom m1),(cod m1)],f] = m1 and
A3: [[(dom m2),(cod m2)],g] = m2 ; ::_thesis: [[(dom m1),(cod m2)],(g * f)] = m2 (*) m1
A4: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13;
then reconsider m19 = m1 as Element of Maps (Hom A) ;
reconsider m29 = m2 as Element of Maps (Hom A) by A4;
A5: cod m19 = (m1 `1) `2 by ENS_1:def_4
.= [(dom m1),(cod m1)] `2 by A2, MCART_1:7
.= dom m2 by A1
.= [(dom m2),(cod m2)] `1
.= (m2 `1) `1 by A3, MCART_1:7
.= dom m29 by ENS_1:def_3 ;
 [[(dom m19),(cod m19)],(m19 `2)] = m1 by ENS_1:8;
then A6: m19 `2 = f by A2, XTUPLE_0:1;
 [[(dom m29),(cod m29)],(m29 `2)] = m2 by ENS_1:8;
then A7: m29 `2 = g by A3, XTUPLE_0:1;
A8: cod m2 = [(dom m2),(cod m2)] `2
.= (m2 `1) `2 by A3, MCART_1:7
.= cod m29 by ENS_1:def_4 ;
A9: dom m19 = (m1 `1) `1 by ENS_1:def_3
.= [(dom m1),(cod m1)] `1 by A2, MCART_1:7
.= dom m1 ;
 [m2,m1] in dom the Comp of (EnsHom A) by A1, CAT_1:15;
then m2 (*) m1 = (fComp (Hom A)) . (m29,m19) by A4, CAT_1:def_1
.= m29 * m19 by A5, ENS_1:def_11
.= [[(dom m1),(cod m2)],(g * f)] by A5, A9, A8, A7, A6, ENS_1:def_6 ;
hence  [[(dom m1),(cod m2)],(g * f)] = m2 (*) m1 ; ::_thesis: verum
end;

definition
let A be Category;
let a be Object of A;
func<|a,?> ->  Functor of A, EnsHom A equals :: YONEDA_1:def 2
 hom?- a;
coherence
 hom?- a is Functor of A, EnsHom A by ENS_1:49;
end;

:: deftheorem  defines <| YONEDA_1:def_2_:_
 for A being Category
for a being Object of A holds <|a,?> = hom?- a;

theorem Th2: :: YONEDA_1:2
for A being Category
for f being Morphism of A holds <|(cod f),?> is_naturally_transformable_to <|(dom f),?>
proof
let A be Category; ::_thesis: for f being Morphism of A holds <|(cod f),?> is_naturally_transformable_to <|(dom f),?>
let f be Morphism of A; ::_thesis: <|(cod f),?> is_naturally_transformable_to <|(dom f),?>
set F1 = <|(cod f),?>;
set F2 = <|(dom f),?>;
set B = EnsHom A;
deffunc H1( Element of A) ->  set = [[(Hom ((cod f),$1)),(Hom ((dom f),$1))],(hom (f,$1))];
A1: for a being Object of A holds [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a))
proof
let a be Object of A; ::_thesis: [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a))
A2: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13;
then reconsider m = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] as Morphism of (EnsHom A) by ENS_1:48;
reconsider m9 = m as Element of Maps (Hom A) by ENS_1:48;
A3: cod m = (fCod (Hom A)) . m by A2
.= cod m9 by ENS_1:def_10
.= (m `1) `2 by ENS_1:def_4
.= [(Hom ((cod f),a)),(Hom ((dom f),a))] `2 by MCART_1:7
.= Hom ((dom f),a)
.= (Obj (hom?- ((Hom A),(dom f)))) . a by ENS_1:60
.= (hom?- ((Hom A),(dom f))) . a
.= <|(dom f),?> . a by ENS_1:def_25 ;
dom m = (fDom (Hom A)) . m by A2
.= dom m9 by ENS_1:def_9
.= (m `1) `1 by ENS_1:def_3
.= [(Hom ((cod f),a)),(Hom ((dom f),a))] `1 by MCART_1:7
.= Hom ((cod f),a)
.= (Obj (hom?- ((Hom A),(cod f)))) . a by ENS_1:60
.= (hom?- ((Hom A),(cod f))) . a
.= <|(cod f),?> . a by ENS_1:def_25 ;
hence  [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A3; ::_thesis: verum
end;
A4: for a being Element of A holds H1(a) in the carrier' of (EnsHom A)
proof
let a be Object of A; ::_thesis: H1(a) in the carrier' of (EnsHom A)
 [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A1;
hence  H1(a) in the carrier' of (EnsHom A) ; ::_thesis: verum
end;
consider t being Function of the carrier of A, the carrier' of (EnsHom A) such that
A5: for o being Element of A holds t . o = H1(o) from FUNCT_2:sch_8(A4);
A6: for a being Object of A holds t . a is Morphism of <|(cod f),?> . a,<|(dom f),?> . a
proof
let a be Object of A; ::_thesis: t . a is Morphism of <|(cod f),?> . a,<|(dom f),?> . a
 [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A1;
then  [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] is Morphism of <|(cod f),?> . a,<|(dom f),?> . a by CAT_1:def_5;
hence  t . a is Morphism of <|(cod f),?> . a,<|(dom f),?> . a by A5; ::_thesis: verum
end;
 for a being Object of A holds Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) <> {} by A1;
then A7: <|(cod f),?> is_transformable_to <|(dom f),?> by NATTRA_1:def_2;
then reconsider t = t as transformation of <|(cod f),?>,<|(dom f),?> by A6, NATTRA_1:def_3;
 for a, b being Object of A st Hom (a,b) <> {} holds
for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)
proof
let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) )
assume A8: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)
A9: Hom ((<|(cod f),?> . a),(<|(cod f),?> . b)) <> {} by A8, CAT_1:84;
let g be Morphism of a,b; ::_thesis: (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)
A10: dom g = a by A8, CAT_1:5;
A11: rng (hom ((cod f),g)) c= dom (hom (f,b))
proof
A12: cod g = b by A8, CAT_1:5;
percases ( Hom ((dom f),b) = {} or Hom ((dom f),b) <> {} ) ;
supposeA13: Hom ((dom f),b) = {} ; ::_thesis: rng (hom ((cod f),g)) c= dom (hom (f,b))
 Hom ((cod f),b) = {} by A13, ENS_1:42;
hence  rng (hom ((cod f),g)) c= dom (hom (f,b)) by A12; ::_thesis: verum
end;
supposeA14: Hom ((dom f),b) <> {} ; ::_thesis: rng (hom ((cod f),g)) c= dom (hom (f,b))
 cod g = b by A8, CAT_1:5;
then A15: ( rng (hom ((cod f),g)) c= Hom ((cod f),(cod g)) & Hom ((cod f),(cod g)) = dom (hom (f,b)) ) by A14, FUNCT_2:def_1, RELAT_1:def_19;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (hom ((cod f),g)) or e in dom (hom (f,b)) )
assume  e in rng (hom ((cod f),g)) ; ::_thesis: e in dom (hom (f,b))
hence  e in dom (hom (f,b)) by A15; ::_thesis: verum
end;
end;
end;
A16: rng (hom (f,a)) c= dom (hom ((dom f),g))
proof
A17: dom g = a by A8, CAT_1:5;
percases ( Hom ((dom f),(cod g)) = {} or Hom ((dom f),(cod g)) <> {} ) ;
supposeA18: Hom ((dom f),(cod g)) = {} ; ::_thesis: rng (hom (f,a)) c= dom (hom ((dom f),g))
 Hom ((dom f),(dom g)) = {} by A18, ENS_1:42;
hence  rng (hom (f,a)) c= dom (hom ((dom f),g)) by A17; ::_thesis: verum
end;
supposeA19: Hom ((dom f),(cod g)) <> {} ; ::_thesis: rng (hom (f,a)) c= dom (hom ((dom f),g))
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (hom (f,a)) or e in dom (hom ((dom f),g)) )
assume A20: e in rng (hom (f,a)) ; ::_thesis: e in dom (hom ((dom f),g))
 ( rng (hom (f,a)) c= Hom ((dom f),a) & Hom ((dom f),a) = dom (hom ((dom f),g)) ) by A17, A19, FUNCT_2:def_1, RELAT_1:def_19;
hence  e in dom (hom ((dom f),g)) by A20; ::_thesis: verum
end;
end;
end;
A21: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))
proof
percases ( Hom ((cod f),(dom g)) = {} or Hom ((cod f),(dom g)) <> {} ) ;
supposeA22: Hom ((cod f),(dom g)) = {} ; ::_thesis: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))
dom ((hom (f,b)) * (hom ((cod f),g))) = dom (hom ((cod f),g)) by A11, RELAT_1:27
.= Hom ((cod f),(dom g)) by A22
.= dom (hom (f,a)) by A10, A22
.= dom ((hom ((dom f),g)) * (hom (f,a))) by A16, RELAT_1:27 ;
hence  dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) ; ::_thesis: verum
end;
supposeA23: Hom ((cod f),(dom g)) <> {} ; ::_thesis: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))
then A24: Hom ((cod f),(cod g)) <> {} by ENS_1:42;
A25: Hom ((dom f),a) <> {} by A10, A23, ENS_1:42;
dom ((hom (f,b)) * (hom ((cod f),g))) = dom (hom ((cod f),g)) by A11, RELAT_1:27
.= Hom ((cod f),(dom g)) by A24, FUNCT_2:def_1
.= Hom ((cod f),a) by A8, CAT_1:5
.= dom (hom (f,a)) by A25, FUNCT_2:def_1
.= dom ((hom ((dom f),g)) * (hom (f,a))) by A16, RELAT_1:27 ;
hence  dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) ; ::_thesis: verum
end;
end;
end;
A26: for x being set st x in dom ((hom (f,b)) * (hom ((cod f),g))) holds
((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x
proof
let x be set ; ::_thesis: ( x in dom ((hom (f,b)) * (hom ((cod f),g))) implies ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x )
assume A27: x in dom ((hom (f,b)) * (hom ((cod f),g))) ; ::_thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x
percases ( Hom ((cod f),(dom g)) <> {} or Hom ((cod f),(dom g)) = {} ) ;
supposeA28: Hom ((cod f),(dom g)) <> {} ; ::_thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x
A29: x in dom (hom ((cod f),g)) by A27, FUNCT_1:11;
 Hom ((cod f),(cod g)) <> {} by A28, ENS_1:42;
then A30: x in Hom ((cod f),(dom g)) by A29, FUNCT_2:def_1;
then reconsider x = x as Morphism of A ;
A31: ( dom g = cod x & dom x = cod f ) by A30, CAT_1:1;
A32: dom g = cod x by A30, CAT_1:1;
then A33: cod (g (*) x) = cod g by CAT_1:17
.= b by A8, CAT_1:5 ;
A34: (hom (f,a)) . x = x (*) f by A10, A30, ENS_1:def_20;
then reconsider h = (hom (f,a)) . x as Morphism of A ;
A35: dom x = cod f by A30, CAT_1:1;
then A36: dom (x (*) f) = dom f by CAT_1:17;
dom (g (*) x) = dom x by A32, CAT_1:17
.= cod f by A30, CAT_1:1 ;
then A37: g (*) x in Hom ((cod f),b) by A33;
cod (x (*) f) = cod x by A35, CAT_1:17
.= dom g by A30, CAT_1:1 ;
then A38: (hom (f,a)) . x in Hom ((dom f),(dom g)) by A34, A36;
((hom (f,b)) * (hom ((cod f),g))) . x = (hom (f,b)) . ((hom ((cod f),g)) . x) by A27, FUNCT_1:12
.= (hom (f,b)) . (g (*) x) by A30, ENS_1:def_19
.= (g (*) x) (*) f by A37, ENS_1:def_20
.= g (*) (x (*) f) by A31, CAT_1:18
.= g (*) h by A10, A30, ENS_1:def_20
.= (hom ((dom f),g)) . ((hom (f,a)) . x) by A38, ENS_1:def_19
.= ((hom ((dom f),g)) * (hom (f,a))) . x by A21, A27, FUNCT_1:12 ;
hence  ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x ; ::_thesis: verum
end;
supposeA39: Hom ((cod f),(dom g)) = {} ; ::_thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x
 x in dom (hom ((cod f),g)) by A27, FUNCT_1:11;
hence  ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x by A39; ::_thesis: verum
end;
end;
end;
A40: Hom ((<|(dom f),?> . a),(<|(dom f),?> . b)) <> {} by A8, CAT_1:84;
A41: cod g = b by A8, CAT_1:5;
reconsider f4 = t . a as Morphism of (EnsHom A) ;
A42: t . a = t . a by A7, NATTRA_1:def_5
.= [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] by A5 ;
then reconsider f49 = f4 as Element of Maps (Hom A) by ENS_1:48;
A43: Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) <> {} by A1;
reconsider f1 = t . b as Morphism of (EnsHom A) ;
A44: t . b = t . b by A7, NATTRA_1:def_5
.= [[(Hom ((cod f),b)),(Hom ((dom f),b))],(hom (f,b))] by A5 ;
then reconsider f19 = f1 as Element of Maps (Hom A) by ENS_1:48;
A45: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13;
then A46: cod f1 = (fCod (Hom A)) . f1
.= cod f19 by ENS_1:def_10
.= (f1 `1) `2 by ENS_1:def_4
.= [(Hom ((cod f),b)),(Hom ((dom f),b))] `2 by A44, MCART_1:7
.= Hom ((dom f),b) ;
A47: dom f4 = (fDom (Hom A)) . f4 by A45
.= dom f49 by ENS_1:def_9
.= (f4 `1) `1 by ENS_1:def_3
.= [(Hom ((cod f),a)),(Hom ((dom f),a))] `1 by A42, MCART_1:7
.= Hom ((cod f),a) ;
A48: cod f4 = (fCod (Hom A)) . f4 by A45
.= cod f49 by ENS_1:def_10
.= (f4 `1) `2 by ENS_1:def_4
.= [(Hom ((cod f),a)),(Hom ((dom f),a))] `2 by A42, MCART_1:7
.= Hom ((dom f),a) ;
reconsider f2 = <|(cod f),?> /. g as Morphism of (EnsHom A) ;
A49: f2 = (hom?- (cod f)) . g by A8, CAT_3:def_10
.= [[(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))],(hom ((cod f),g))] by ENS_1:def_21 ;
then reconsider f29 = f2 as Element of Maps (Hom A) by ENS_1:47;
A50: dom f2 = (fDom (Hom A)) . f2 by A45
.= dom f29 by ENS_1:def_9
.= (f2 `1) `1 by ENS_1:def_3
.= [(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))] `1 by A49, MCART_1:7
.= Hom ((cod f),(dom g)) ;
A51: cod f2 = (fCod (Hom A)) . f2 by A45
.= cod f29 by ENS_1:def_10
.= (f2 `1) `2 by ENS_1:def_4
.= [(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))] `2 by A49, MCART_1:7
.= Hom ((cod f),(cod g)) ;
A52: dom f1 = (fDom (Hom A)) . f1 by A45
.= dom f19 by ENS_1:def_9
.= (f1 `1) `1 by ENS_1:def_3
.= [(Hom ((cod f),b)),(Hom ((dom f),b))] `1 by A44, MCART_1:7
.= Hom ((cod f),b) ;
then A53: cod f2 = dom f1 by A8, A51, CAT_1:5;
reconsider f3 = <|(dom f),?> /. g as Morphism of (EnsHom A) ;
A54: f3 = (hom?- (dom f)) . g by A8, CAT_3:def_10
.= [[(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))],(hom ((dom f),g))] by ENS_1:def_21 ;
then reconsider f39 = f3 as Element of Maps (Hom A) by ENS_1:47;
A55: cod f3 = (fCod (Hom A)) . f3 by A45
.= cod f39 by ENS_1:def_10
.= (f3 `1) `2 by ENS_1:def_4
.= [(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))] `2 by A54, MCART_1:7
.= Hom ((dom f),(cod g)) ;
A56: dom f3 = (fDom (Hom A)) . f3 by A45
.= dom f39 by ENS_1:def_9
.= (f3 `1) `1 by ENS_1:def_3
.= [(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))] `1 by A54, MCART_1:7
.= Hom ((dom f),(dom g)) ;
then A57: cod f4 = dom f3 by A8, A48, CAT_1:5;
 Hom ((<|(cod f),?> . b),(<|(dom f),?> . b)) <> {} by A1;
then (t . b) * (<|(cod f),?> /. g) = f1 (*) f2 by A9, CAT_1:def_13
.= [[(Hom ((cod f),(dom g))),(Hom ((dom f),b))],((hom (f,b)) * (hom ((cod f),g)))] by A44, A52, A46, A49, A50, A51, A53, Th1
.= [[(Hom ((cod f),a)),(Hom ((dom f),(cod g)))],((hom ((dom f),g)) * (hom (f,a)))] by A10, A41, A21, A26, FUNCT_1:2
.= f3 (*) f4 by A54, A56, A55, A42, A47, A48, A57, Th1
.= (<|(dom f),?> /. g) * (t . a) by A40, A43, CAT_1:def_13 ;
hence  (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) ; ::_thesis: verum
end;
hence  <|(cod f),?> is_naturally_transformable_to <|(dom f),?> by A7, NATTRA_1:def_7; ::_thesis: verum
end;

definition
let A be Category;
let f be Morphism of A;
func<|f,?> ->  natural_transformation of <|(cod f),?>,<|(dom f),?> means :Def3: :: YONEDA_1:def 3
 for o being Object of A holds it . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))];
existence
 ex b1 being natural_transformation of <|(cod f),?>,<|(dom f),?> st
for o being Object of A holds b1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))]
proof
set B = EnsHom A;
deffunc H1( Element of A) ->  set = [[(Hom ((cod f),$1)),(Hom ((dom f),$1))],(hom (f,(id $1)))];
set F1 = <|(cod f),?>;
set F2 = <|(dom f),?>;
A1: for o being Object of A holds [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom ((<|(cod f),?> . o),(<|(dom f),?> . o))
proof
let o be Object of A; ::_thesis: [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom ((<|(cod f),?> . o),(<|(dom f),?> . o))
A2: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13;
A3: hom (f,(id o)) = hom (f,o) by ENS_1:53;
then reconsider m = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] as Morphism of (EnsHom A) by A2, ENS_1:48;
reconsider m9 = m as Element of Maps (Hom A) by A3, ENS_1:48;
A4: cod m = (fCod (Hom A)) . m by A2
.= cod m9 by ENS_1:def_10
.= (m `1) `2 by ENS_1:def_4
.= [(Hom ((cod f),o)),(Hom ((dom f),o))] `2 by MCART_1:7
.= Hom ((dom f),o)
.= (Obj (hom?- ((Hom A),(dom f)))) . o by ENS_1:60
.= (hom?- ((Hom A),(dom f))) . o
.= <|(dom f),?> . o by ENS_1:def_25 ;
dom m = (fDom (Hom A)) . m by A2
.= dom m9 by ENS_1:def_9
.= (m `1) `1 by ENS_1:def_3
.= [(Hom ((cod f),o)),(Hom ((dom f),o))] `1 by MCART_1:7
.= Hom ((cod f),o)
.= (Obj (hom?- ((Hom A),(cod f)))) . o by ENS_1:60
.= (hom?- ((Hom A),(cod f))) . o
.= <|(cod f),?> . o by ENS_1:def_25 ;
hence  [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) by A4; ::_thesis: verum
end;
A5: for o being Element of A holds H1(o) in the carrier' of (EnsHom A)
proof
let o be Object of A; ::_thesis: H1(o) in the carrier' of (EnsHom A)
 [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) by A1;
hence  H1(o) in the carrier' of (EnsHom A) ; ::_thesis: verum
end;
consider t being Function of the carrier of A, the carrier' of (EnsHom A) such that
A6: for o being Element of A holds t . o = H1(o) from FUNCT_2:sch_8(A5);
A7: for o being Object of A holds t . o is Morphism of <|(cod f),?> . o,<|(dom f),?> . o
proof
let o be Object of A; ::_thesis: t . o is Morphism of <|(cod f),?> . o,<|(dom f),?> . o
 [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) by A1;
then  [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] is Morphism of <|(cod f),?> . o,<|(dom f),?> . o by CAT_1:def_5;
hence  t . o is Morphism of <|(cod f),?> . o,<|(dom f),?> . o by A6; ::_thesis: verum
end;
 for o being Object of A holds Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) <> {} by A1;
then A8: <|(cod f),?> is_transformable_to <|(dom f),?> by NATTRA_1:def_2;
then reconsider t = t as transformation of <|(cod f),?>,<|(dom f),?> by A7, NATTRA_1:def_3;
A9: for a, b being Object of A st Hom (a,b) <> {} holds
for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)
proof
let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) )
assume A10: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)
A11: Hom ((<|(cod f),?> . a),(<|(cod f),?> . b)) <> {} by A10, CAT_1:84;
let g be Morphism of a,b; ::_thesis: (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)
A12: dom g = a by A10, CAT_1:5;
A13: rng (hom ((cod f),g)) c= dom (hom (f,b))
proof
A14: cod g = b by A10, CAT_1:5;
percases ( Hom ((dom f),b) = {} or Hom ((dom f),b) <> {} ) ;
supposeA15: Hom ((dom f),b) = {} ; ::_thesis: rng (hom ((cod f),g)) c= dom (hom (f,b))
 Hom ((cod f),b) = {} by A15, ENS_1:42;
hence  rng (hom ((cod f),g)) c= dom (hom (f,b)) by A14; ::_thesis: verum
end;
supposeA16: Hom ((dom f),b) <> {} ; ::_thesis: rng (hom ((cod f),g)) c= dom (hom (f,b))
 cod g = b by A10, CAT_1:5;
then A17: ( rng (hom ((cod f),g)) c= Hom ((cod f),(cod g)) & Hom ((cod f),(cod g)) = dom (hom (f,b)) ) by A16, FUNCT_2:def_1, RELAT_1:def_19;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (hom ((cod f),g)) or e in dom (hom (f,b)) )
assume  e in rng (hom ((cod f),g)) ; ::_thesis: e in dom (hom (f,b))
hence  e in dom (hom (f,b)) by A17; ::_thesis: verum
end;
end;
end;
A18: rng (hom (f,a)) c= dom (hom ((dom f),g))
proof
A19: dom g = a by A10, CAT_1:5;
percases ( Hom ((dom f),(cod g)) = {} or Hom ((dom f),(cod g)) <> {} ) ;
supposeA20: Hom ((dom f),(cod g)) = {} ; ::_thesis: rng (hom (f,a)) c= dom (hom ((dom f),g))
 Hom ((dom f),(dom g)) = {} by A20, ENS_1:42;
hence  rng (hom (f,a)) c= dom (hom ((dom f),g)) by A19; ::_thesis: verum
end;
supposeA21: Hom ((dom f),(cod g)) <> {} ; ::_thesis: rng (hom (f,a)) c= dom (hom ((dom f),g))
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (hom (f,a)) or e in dom (hom ((dom f),g)) )
assume A22: e in rng (hom (f,a)) ; ::_thesis: e in dom (hom ((dom f),g))
 ( rng (hom (f,a)) c= Hom ((dom f),a) & Hom ((dom f),a) = dom (hom ((dom f),g)) ) by A19, A21, FUNCT_2:def_1, RELAT_1:def_19;
hence  e in dom (hom ((dom f),g)) by A22; ::_thesis: verum
end;
end;
end;
A23: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))
proof
percases ( Hom ((cod f),(dom g)) = {} or Hom ((cod f),(dom g)) <> {} ) ;
supposeA24: Hom ((cod f),(dom g)) = {} ; ::_thesis: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))
dom ((hom (f,b)) * (hom ((cod f),g))) = dom (hom ((cod f),g)) by A13, RELAT_1:27
.= Hom ((cod f),a) by A12, A24
.= dom (hom (f,a)) by A12, A24
.= dom ((hom ((dom f),g)) * (hom (f,a))) by A18, RELAT_1:27 ;
hence  dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) ; ::_thesis: verum
end;
supposeA25: Hom ((cod f),(dom g)) <> {} ; ::_thesis: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))
then A26: Hom ((cod f),(cod g)) <> {} by ENS_1:42;
A27: Hom ((dom f),a) <> {} by A12, A25, ENS_1:42;
dom ((hom (f,b)) * (hom ((cod f),g))) = dom (hom ((cod f),g)) by A13, RELAT_1:27
.= Hom ((cod f),a) by A12, A26, FUNCT_2:def_1
.= dom (hom (f,a)) by A27, FUNCT_2:def_1
.= dom ((hom ((dom f),g)) * (hom (f,a))) by A18, RELAT_1:27 ;
hence  dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) ; ::_thesis: verum
end;
end;
end;
A28: for x being set st x in dom ((hom (f,b)) * (hom ((cod f),g))) holds
((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x
proof
let x be set ; ::_thesis: ( x in dom ((hom (f,b)) * (hom ((cod f),g))) implies ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x )
assume A29: x in dom ((hom (f,b)) * (hom ((cod f),g))) ; ::_thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x
percases ( Hom ((cod f),(dom g)) <> {} or Hom ((cod f),(dom g)) = {} ) ;
supposeA30: Hom ((cod f),(dom g)) <> {} ; ::_thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x
A31: x in dom (hom ((cod f),g)) by A29, FUNCT_1:11;
 Hom ((cod f),(cod g)) <> {} by A30, ENS_1:42;
then A32: x in Hom ((cod f),(dom g)) by A31, FUNCT_2:def_1;
then reconsider x = x as Morphism of A ;
A33: dom g = cod x by A32, CAT_1:1;
 cod g = b by A10, CAT_1:5;
then A34: cod (g (*) x) = b by A33, CAT_1:17;
dom (g (*) x) = dom x by A33, CAT_1:17
.= cod f by A32, CAT_1:1 ;
then A35: g (*) x in Hom ((cod f),b) by A34;
A36: dom x = cod f by A32, CAT_1:1;
then A37: dom (x (*) f) = dom f by CAT_1:17;
A38: (hom (f,a)) . x = x (*) f by A12, A32, ENS_1:def_20;
then reconsider h = (hom (f,a)) . x as Morphism of A ;
A39: ( dom g = cod x & dom x = cod f ) by A32, CAT_1:1;
cod (x (*) f) = cod x by A36, CAT_1:17
.= dom g by A32, CAT_1:1 ;
then A40: (hom (f,a)) . x in Hom ((dom f),(dom g)) by A38, A37;
((hom (f,b)) * (hom ((cod f),g))) . x = (hom (f,b)) . ((hom ((cod f),g)) . x) by A29, FUNCT_1:12
.= (hom (f,b)) . (g (*) x) by A32, ENS_1:def_19
.= (g (*) x) (*) f by A35, ENS_1:def_20
.= g (*) (x (*) f) by A39, CAT_1:18
.= g (*) h by A12, A32, ENS_1:def_20
.= (hom ((dom f),g)) . ((hom (f,a)) . x) by A40, ENS_1:def_19
.= ((hom ((dom f),g)) * (hom (f,a))) . x by A23, A29, FUNCT_1:12 ;
hence  ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x ; ::_thesis: verum
end;
supposeA41: Hom ((cod f),(dom g)) = {} ; ::_thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x
 x in dom (hom ((cod f),g)) by A29, FUNCT_1:11;
hence  ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x by A41; ::_thesis: verum
end;
end;
end;
A42: Hom ((<|(dom f),?> . a),(<|(dom f),?> . b)) <> {} by A10, CAT_1:84;
A43: cod g = b by A10, CAT_1:5;
reconsider f4 = t . a as Morphism of (EnsHom A) ;
A44: t . a = t . a by A8, NATTRA_1:def_5
.= [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,(id a)))] by A6
.= [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] by ENS_1:53 ;
then reconsider f49 = f4 as Element of Maps (Hom A) by ENS_1:48;
A45: Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) <> {} by A1;
reconsider f1 = t . b as Morphism of (EnsHom A) ;
A46: t . b = t . b by A8, NATTRA_1:def_5
.= [[(Hom ((cod f),b)),(Hom ((dom f),b))],(hom (f,(id b)))] by A6
.= [[(Hom ((cod f),b)),(Hom ((dom f),b))],(hom (f,b))] by ENS_1:53 ;
then reconsider f19 = f1 as Element of Maps (Hom A) by ENS_1:48;
A47: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13;
then A48: cod f1 = (fCod (Hom A)) . f1
.= cod f19 by ENS_1:def_10
.= (f1 `1) `2 by ENS_1:def_4
.= [(Hom ((cod f),b)),(Hom ((dom f),b))] `2 by A46, MCART_1:7
.= Hom ((dom f),b) ;
A49: dom f4 = (fDom (Hom A)) . f4 by A47
.= dom f49 by ENS_1:def_9
.= (f4 `1) `1 by ENS_1:def_3
.= [(Hom ((cod f),a)),(Hom ((dom f),a))] `1 by A44, MCART_1:7
.= Hom ((cod f),a) ;
A50: cod f4 = (fCod (Hom A)) . f4 by A47
.= cod f49 by ENS_1:def_10
.= (f4 `1) `2 by ENS_1:def_4
.= [(Hom ((cod f),a)),(Hom ((dom f),a))] `2 by A44, MCART_1:7
.= Hom ((dom f),a) ;
reconsider f2 = <|(cod f),?> /. g as Morphism of (EnsHom A) ;
A51: f2 = (hom?- (cod f)) . g by A10, CAT_3:def_10
.= [[(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))],(hom ((cod f),g))] by ENS_1:def_21 ;
then reconsider f29 = f2 as Element of Maps (Hom A) by ENS_1:47;
A52: dom f2 = (fDom (Hom A)) . f2 by A47
.= dom f29 by ENS_1:def_9
.= (f2 `1) `1 by ENS_1:def_3
.= [(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))] `1 by A51, MCART_1:7
.= Hom ((cod f),(dom g)) ;
A53: cod f2 = (fCod (Hom A)) . f2 by A47
.= cod f29 by ENS_1:def_10
.= (f2 `1) `2 by ENS_1:def_4
.= [(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))] `2 by A51, MCART_1:7
.= Hom ((cod f),(cod g)) ;
A54: dom f1 = (fDom (Hom A)) . f1 by A47
.= dom f19 by ENS_1:def_9
.= (f1 `1) `1 by ENS_1:def_3
.= [(Hom ((cod f),b)),(Hom ((dom f),b))] `1 by A46, MCART_1:7
.= Hom ((cod f),b) ;
then A55: cod f2 = dom f1 by A10, A53, CAT_1:5;
reconsider f3 = <|(dom f),?> /. g as Morphism of (EnsHom A) ;
A56: f3 = (hom?- (dom f)) . g by A10, CAT_3:def_10
.= [[(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))],(hom ((dom f),g))] by ENS_1:def_21 ;
then reconsider f39 = f3 as Element of Maps (Hom A) by ENS_1:47;
A57: cod f3 = (fCod (Hom A)) . f3 by A47
.= cod f39 by ENS_1:def_10
.= (f3 `1) `2 by ENS_1:def_4
.= [(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))] `2 by A56, MCART_1:7
.= Hom ((dom f),(cod g)) ;
A58: dom f3 = (fDom (Hom A)) . f3 by A47
.= dom f39 by ENS_1:def_9
.= (f3 `1) `1 by ENS_1:def_3
.= [(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))] `1 by A56, MCART_1:7
.= Hom ((dom f),(dom g)) ;
then A59: cod f4 = dom f3 by A10, A50, CAT_1:5;
 Hom ((<|(cod f),?> . b),(<|(dom f),?> . b)) <> {} by A1;
then (t . b) * (<|(cod f),?> /. g) = f1 (*) f2 by A11, CAT_1:def_13
.= [[(Hom ((cod f),(dom g))),(Hom ((dom f),b))],((hom (f,b)) * (hom ((cod f),g)))] by A46, A54, A48, A51, A52, A53, A55, Th1
.= [[(Hom ((cod f),a)),(Hom ((dom f),(cod g)))],((hom ((dom f),g)) * (hom (f,a)))] by A12, A43, A23, A28, FUNCT_1:2
.= f3 (*) f4 by A56, A58, A57, A44, A49, A50, A59, Th1
.= (<|(dom f),?> /. g) * (t . a) by A42, A45, CAT_1:def_13 ;
hence  (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) ; ::_thesis: verum
end;
 <|(cod f),?> is_naturally_transformable_to <|(dom f),?> by Th2;
then reconsider t = t as natural_transformation of <|(cod f),?>,<|(dom f),?> by A9, NATTRA_1:def_8;
 for o being Element of A holds t . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))]
proof
let o be Object of A; ::_thesis: t . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))]
t . o = t . o by A8, NATTRA_1:def_5
.= [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] by A6 ;
hence  t . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ; ::_thesis: verum
end;
hence  ex b1 being natural_transformation of <|(cod f),?>,<|(dom f),?> st
for o being Object of A holds b1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being natural_transformation of <|(cod f),?>,<|(dom f),?> st ( for o being Object of A holds b1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) & ( for o being Object of A holds b2 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) holds
b1 = b2
proof
 for a being Object of A holds [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a))
proof
let a be Object of A; ::_thesis: [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a))
A60: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13;
then reconsider m = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] as Morphism of (EnsHom A) by ENS_1:48;
reconsider m9 = m as Element of Maps (Hom A) by ENS_1:48;
A61: cod m = (fCod (Hom A)) . m by A60
.= cod m9 by ENS_1:def_10
.= (m `1) `2 by ENS_1:def_4
.= [(Hom ((cod f),a)),(Hom ((dom f),a))] `2 by MCART_1:7
.= Hom ((dom f),a)
.= (Obj (hom?- ((Hom A),(dom f)))) . a by ENS_1:60
.= (hom?- ((Hom A),(dom f))) . a
.= <|(dom f),?> . a by ENS_1:def_25 ;
dom m = (fDom (Hom A)) . m by A60
.= dom m9 by ENS_1:def_9
.= (m `1) `1 by ENS_1:def_3
.= [(Hom ((cod f),a)),(Hom ((dom f),a))] `1 by MCART_1:7
.= Hom ((cod f),a)
.= (Obj (hom?- ((Hom A),(cod f)))) . a by ENS_1:60
.= (hom?- ((Hom A),(cod f))) . a
.= <|(cod f),?> . a by ENS_1:def_25 ;
hence  [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A61; ::_thesis: verum
end;
then  for a being Object of A holds Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) <> {} ;
then A62: <|(cod f),?> is_transformable_to <|(dom f),?> by NATTRA_1:def_2;
let h1, h2 be natural_transformation of <|(cod f),?>,<|(dom f),?>; ::_thesis: ( ( for o being Object of A holds h1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) & ( for o being Object of A holds h2 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) implies h1 = h2 )
assume that
A63: for o being Object of A holds h1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] and
A64: for o being Object of A holds h2 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ; ::_thesis: h1 = h2
now__::_thesis:_for_o_being_Object_of_A_holds_h1_._o_=_h2_._o
let o be Object of A; ::_thesis: h1 . o = h2 . o
thus h1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] by A63
.= h2 . o by A64 ; ::_thesis: verum
end;
hence  h1 = h2 by A62, NATTRA_1:19; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines <| YONEDA_1:def_3_:_
 for A being Category
for f being Morphism of A
for b3 being natural_transformation of <|(cod f),?>,<|(dom f),?> holds
( b3 = <|f,?> iff for o being Object of A holds b3 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] );

theorem Th3: :: YONEDA_1:3
for A being Category
for f being Element of the carrier' of A holds [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Element of the carrier' of (Functors (A,(EnsHom A)))
proof
let A be Category; ::_thesis: for f being Element of the carrier' of A holds [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Element of the carrier' of (Functors (A,(EnsHom A)))
let f be Element of the carrier' of A; ::_thesis: [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Element of the carrier' of (Functors (A,(EnsHom A)))
 <|(cod f),?> is_naturally_transformable_to <|(dom f),?> by Th2;
then  [[<|(cod f),?>,<|(dom f),?>],<|f,?>] in NatTrans (A,(EnsHom A)) by NATTRA_1:def_16;
hence  [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Element of the carrier' of (Functors (A,(EnsHom A))) by NATTRA_1:def_17; ::_thesis: verum
end;

definition
let A be Category;
func Yoneda A ->  Contravariant_Functor of A, Functors (A,(EnsHom A)) means :Def4: :: YONEDA_1:def 4
 for f being Morphism of A holds it . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>];
existence
 ex b1 being Contravariant_Functor of A, Functors (A,(EnsHom A)) st
for f being Morphism of A holds b1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>]
proof
deffunc H1( Element of the carrier' of A) ->  set = [[<|(cod $1),?>,<|(dom $1),?>],<|$1,?>];
A1: for f being Element of the carrier' of A holds H1(f) in the carrier' of (Functors (A,(EnsHom A)))
proof
let f be Morphism of A; ::_thesis: H1(f) in the carrier' of (Functors (A,(EnsHom A)))
 [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Morphism of (Functors (A,(EnsHom A))) by Th3;
hence  H1(f) in the carrier' of (Functors (A,(EnsHom A))) ; ::_thesis: verum
end;
consider F being Function of the carrier' of A, the carrier' of (Functors (A,(EnsHom A))) such that
A2: for f being Element of the carrier' of A holds F . f = H1(f) from FUNCT_2:sch_8(A1);
A3: for f, g being Morphism of A st dom g = cod f holds
F . (g (*) f) = (F . f) (*) (F . g)
proof
let f, g be Morphism of A; ::_thesis: ( dom g = cod f implies F . (g (*) f) = (F . f) (*) (F . g) )
reconsider t1 = <|g,?> as natural_transformation of <|(cod g),?>,<|(dom g),?> ;
assume A4: dom g = cod f ; ::_thesis: F . (g (*) f) = (F . f) (*) (F . g)
then reconsider t = <|f,?> as natural_transformation of <|(dom g),?>,<|(dom f),?> ;
A5: F . g = [[<|(cod g),?>,<|(dom g),?>],t1] by A2;
A6: dom (g (*) f) = dom f by A4, CAT_1:17;
then reconsider tt = t `*` t1 as natural_transformation of <|(cod (g (*) f)),?>,<|(dom (g (*) f)),?> by A4, CAT_1:17;
A7: cod (g (*) f) = cod g by A4, CAT_1:17;
 for o being Object of A holds <|(g (*) f),?> . o = tt . o
proof
set F1 = <|(cod f),?>;
set F2 = <|(dom f),?>;
let o be Object of A; ::_thesis: <|(g (*) f),?> . o = tt . o
reconsider f1 = t . o as Morphism of (EnsHom A) ;
reconsider f2 = t1 . o as Morphism of (EnsHom A) ;
A8: f2 = [[(Hom ((cod g),o)),(Hom ((dom g),o))],(hom (g,(id o)))] by Def3;
 for a being Object of A holds [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom ((<|(cod g),?> . a),(<|(dom g),?> . a))
proof
let a be Object of A; ::_thesis: [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom ((<|(cod g),?> . a),(<|(dom g),?> . a))
A9: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13;
then reconsider m = [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] as Morphism of (EnsHom A) by ENS_1:48;
reconsider m9 = m as Element of Maps (Hom A) by ENS_1:48;
A10: cod m = (fCod (Hom A)) . m by A9
.= cod m9 by ENS_1:def_10
.= (m `1) `2 by ENS_1:def_4
.= [(Hom ((cod g),a)),(Hom ((dom g),a))] `2 by MCART_1:7
.= Hom ((dom g),a)
.= (Obj (hom?- ((Hom A),(dom g)))) . a by ENS_1:60
.= (hom?- ((Hom A),(dom g))) . a
.= <|(dom g),?> . a by ENS_1:def_25 ;
dom m = (fDom (Hom A)) . m by A9
.= dom m9 by ENS_1:def_9
.= (m `1) `1 by ENS_1:def_3
.= [(Hom ((cod g),a)),(Hom ((dom g),a))] `1 by MCART_1:7
.= Hom ((cod g),a)
.= (Obj (hom?- ((Hom A),(cod g)))) . a by ENS_1:60
.= (hom?- ((Hom A),(cod g))) . a
.= <|(cod g),?> . a by ENS_1:def_25 ;
hence  [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom ((<|(cod g),?> . a),(<|(dom g),?> . a)) by A10; ::_thesis: verum
end;
then A11: Hom ((<|(cod g),?> . o),(<|(dom g),?> . o)) <> {} ;
 for a being Object of A holds [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a))
proof
let a be Object of A; ::_thesis: [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a))
A12: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13;
then reconsider m = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] as Morphism of (EnsHom A) by ENS_1:48;
reconsider m9 = m as Element of Maps (Hom A) by ENS_1:48;
A13: cod m = (fCod (Hom A)) . m by A12
.= cod m9 by ENS_1:def_10
.= (m `1) `2 by ENS_1:def_4
.= [(Hom ((cod f),a)),(Hom ((dom f),a))] `2 by MCART_1:7
.= Hom ((dom f),a)
.= (Obj (hom?- ((Hom A),(dom f)))) . a by ENS_1:60
.= (hom?- ((Hom A),(dom f))) . a
.= <|(dom f),?> . a by ENS_1:def_25 ;
dom m = (fDom (Hom A)) . m by A12
.= dom m9 by ENS_1:def_9
.= (m `1) `1 by ENS_1:def_3
.= [(Hom ((cod f),a)),(Hom ((dom f),a))] `1 by MCART_1:7
.= Hom ((cod f),a)
.= (Obj (hom?- ((Hom A),(cod f)))) . a by ENS_1:60
.= (hom?- ((Hom A),(cod f))) . a
.= <|(cod f),?> . a by ENS_1:def_25 ;
hence  [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A13; ::_thesis: verum
end;
then A14: Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) <> {} ;
A15: <|(g (*) f),?> . o = [[(Hom ((cod g),o)),(Hom ((dom (g (*) f)),o))],(hom ((g (*) f),(id o)))] by A7, Def3
.= [[(Hom ((cod g),o)),(Hom ((dom f),o))],(hom ((g (*) f),o))] by A6, ENS_1:53 ;
A16: t . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] by A4, Def3;
A17: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13;
then reconsider f19 = f1 as Element of Maps (Hom A) ;
reconsider f29 = f2 as Element of Maps (Hom A) by A17;
A18: cod f2 = (fCod (Hom A)) . f2 by A17
.= cod f29 by ENS_1:def_10
.= (f2 `1) `2 by ENS_1:def_4
.= [(Hom ((cod g),o)),(Hom ((dom g),o))] `2 by A8, MCART_1:7
.= Hom ((dom g),o) ;
A19: cod f1 = (fCod (Hom A)) . f1 by A17
.= cod f19 by ENS_1:def_10
.= (f1 `1) `2 by ENS_1:def_4
.= [(Hom ((cod f),o)),(Hom ((dom f),o))] `2 by A16, MCART_1:7
.= Hom ((dom f),o) ;
A20: dom f1 = (fDom (Hom A)) . f1 by A17
.= dom f19 by ENS_1:def_9
.= (f1 `1) `1 by ENS_1:def_3
.= [(Hom ((cod f),o)),(Hom ((dom f),o))] `1 by A16, MCART_1:7
.= Hom ((cod f),o) ;
A21: dom f2 = (fDom (Hom A)) . f2 by A17
.= dom f29 by ENS_1:def_9
.= (f2 `1) `1 by ENS_1:def_3
.= [(Hom ((cod g),o)),(Hom ((dom g),o))] `1 by A8, MCART_1:7
.= Hom ((cod g),o) ;
 ( <|(dom g),?> is_naturally_transformable_to <|(dom f),?> & <|(cod g),?> is_naturally_transformable_to <|(dom g),?> ) by A4, Th2;
then tt . o = (t . o) * (t1 . o) by A6, A7, NATTRA_1:25
.= f1 (*) f2 by A4, A14, A11, CAT_1:def_13
.= [[(Hom ((cod g),o)),(Hom ((dom f),o))],((hom (f,(id o))) * (hom (g,(id o))))] by A4, A16, A8, A20, A18, A21, A19, Th1
.= [[(Hom ((cod g),o)),(Hom ((dom f),o))],((hom (f,o)) * (hom (g,(id o))))] by ENS_1:53
.= [[(Hom ((cod g),o)),(Hom ((dom f),o))],((hom (f,o)) * (hom (g,o)))] by ENS_1:53
.= [[(Hom ((cod g),o)),(Hom ((dom f),o))],(hom ((g (*) f),o))] by A4, ENS_1:46 ;
hence  <|(g (*) f),?> . o = tt . o by A15; ::_thesis: verum
end;
then A22: <|(g (*) f),?> = tt by Th2, ISOCAT_1:26;
A23: F . f = [[<|(dom g),?>,<|(dom f),?>],t] by A2, A4;
then A24: [(F . f),(F . g)] in dom the Comp of (Functors (A,(EnsHom A))) by A5, NATTRA_1:35;
then consider F9, F19, F29 being Functor of A, EnsHom A, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A25: F . g = [[F9,F19],t9] and
A26: F . f = [[F19,F29],t19] and
A27: the Comp of (Functors (A,(EnsHom A))) . ((F . f),(F . g)) = [[F9,F29],(t19 `*` t9)] by NATTRA_1:def_17;
A28: <|f,?> = t19 by A23, A26, XTUPLE_0:1;
 [F19,F29] = [<|(dom g),?>,<|(dom f),?>] by A23, A26, XTUPLE_0:1;
then A29: <|(dom f),?> = F29 by XTUPLE_0:1;
 [F9,F19] = [<|(cod g),?>,<|(dom g),?>] by A5, A25, XTUPLE_0:1;
then A30: ( <|(cod g),?> = F9 & <|(dom g),?> = F19 ) by XTUPLE_0:1;
 <|g,?> = t9 by A5, A25, XTUPLE_0:1;
then  (F . f) (*) (F . g) = [[<|(cod g),?>,<|(dom f),?>],(t `*` t1)] by A24, A27, A28, A30, A29, CAT_1:def_1;
hence  F . (g (*) f) = (F . f) (*) (F . g) by A2, A6, A7, A22; ::_thesis: verum
end;
A31: for f being Morphism of A holds
( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) )
proof
let f be Morphism of A; ::_thesis: ( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) )
set g = F . f;
set X = dom <|(id (dom f)),?>;
A32: dom <|(id (dom f)),?> = the carrier of A by FUNCT_2:def_1
.= dom (id <|(dom f),?>) by FUNCT_2:def_1 ;
A33: F . (id (dom f)) = [[<|(cod (id (dom f))),?>,<|(dom (id (dom f))),?>],<|(id (dom f)),?>] by A2
.= [[<|(dom f),?>,<|(dom (id (dom f))),?>],<|(id (dom f)),?>] by CAT_1:58
.= [[<|(dom f),?>,<|(dom f),?>],<|(id (dom f)),?>] by CAT_1:58 ;
A34: F . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] by A2;
then  cod (F . f) = <|(dom f),?> by NATTRA_1:33;
then A35: [[<|(dom f),?>,<|(dom f),?>],(id <|(dom f),?>)] = id (cod (F . f)) by NATTRA_1:def_17;
A36: for y being set st y in dom <|(id (dom f)),?> holds
<|(id (dom f)),?> . y = (id <|(dom f),?>) . y
proof
let y be set ; ::_thesis: ( y in dom <|(id (dom f)),?> implies <|(id (dom f)),?> . y = (id <|(dom f),?>) . y )
assume  y in dom <|(id (dom f)),?> ; ::_thesis: <|(id (dom f)),?> . y = (id <|(dom f),?>) . y
then reconsider z = y as Object of A by FUNCT_2:def_1;
reconsider zz = id z as Morphism of z,z ;
A37: Hom (z,z) <> {} ;
A38: <|(cod (id (dom f))),?> is_transformable_to <|(dom (id (dom f))),?> ;
<|(id (dom f)),?> . z = [[(Hom ((cod (id (dom f))),z)),(Hom ((dom (id (dom f))),z))],(hom ((id (dom f)),(id z)))] by Def3
.= [[(Hom ((dom f),z)),(Hom ((dom (id (dom f))),z))],(hom ((id (dom f)),(id z)))]
.= [[(Hom ((dom f),z)),(Hom ((dom f),z))],(hom ((id (dom f)),(id z)))]
.= [[(Hom ((dom f),z)),(Hom ((dom f),z))],(hom ((dom f),(id z)))] by ENS_1:53
.= [[(Hom ((dom f),z)),(Hom ((dom f),(cod (id z))))],(hom ((dom f),(id z)))]
.= [[(Hom ((dom f),(dom (id z)))),(Hom ((dom f),(cod (id z))))],(hom ((dom f),(id z)))]
.= <|(dom f),?> . (id z) by ENS_1:def_21
.= <|(dom f),?> /. zz by A37, CAT_3:def_10
.= id (<|(dom f),?> . z) by NATTRA_1:15
.= (id <|(dom f),?>) . z by NATTRA_1:20
.= (id <|(dom f),?>) . z by NATTRA_1:def_5 ;
hence  <|(id (dom f)),?> . y = (id <|(dom f),?>) . y by A38, NATTRA_1:def_5; ::_thesis: verum
end;
set X = dom <|(id (cod f)),?>;
A39: for y being set st y in dom <|(id (cod f)),?> holds
<|(id (cod f)),?> . y = (id <|(cod f),?>) . y
proof
let y be set ; ::_thesis: ( y in dom <|(id (cod f)),?> implies <|(id (cod f)),?> . y = (id <|(cod f),?>) . y )
assume  y in dom <|(id (cod f)),?> ; ::_thesis: <|(id (cod f)),?> . y = (id <|(cod f),?>) . y
then reconsider z = y as Object of A by FUNCT_2:def_1;
A40: Hom (z,z) <> {} ;
A41: <|(cod (id (cod f))),?> is_transformable_to <|(dom (id (cod f))),?> ;
<|(id (cod f)),?> . z = [[(Hom ((cod (id (cod f))),z)),(Hom ((dom (id (cod f))),z))],(hom ((id (cod f)),(id z)))] by Def3
.= [[(Hom ((cod f),z)),(Hom ((dom (id (cod f))),z))],(hom ((id (cod f)),(id z)))]
.= [[(Hom ((cod f),z)),(Hom ((cod f),z))],(hom ((id (cod f)),(id z)))]
.= [[(Hom ((cod f),z)),(Hom ((cod f),z))],(hom ((cod f),(id z)))] by ENS_1:53
.= [[(Hom ((cod f),z)),(Hom ((cod f),(cod (id z))))],(hom ((cod f),(id z)))]
.= [[(Hom ((cod f),(dom (id z)))),(Hom ((cod f),(cod (id z))))],(hom ((cod f),(id z)))]
.= <|(cod f),?> . (id z) by ENS_1:def_21
.= <|(cod f),?> /. (id z) by A40, CAT_3:def_10
.= id (<|(cod f),?> . z) by NATTRA_1:15
.= (id <|(cod f),?>) . z by NATTRA_1:20
.= (id <|(cod f),?>) . z by NATTRA_1:def_5 ;
hence  <|(id (cod f)),?> . y = (id <|(cod f),?>) . y by A41, NATTRA_1:def_5; ::_thesis: verum
end;
dom <|(id (cod f)),?> = the carrier of A by FUNCT_2:def_1
.= dom (id <|(cod f),?>) by FUNCT_2:def_1 ;
then A42: <|(id (cod f)),?> = id <|(cod f),?> by A39, FUNCT_1:2;
A43: F . (id (cod f)) = [[<|(cod (id (cod f))),?>,<|(dom (id (cod f))),?>],<|(id (cod f)),?>] by A2
.= [[<|(cod f),?>,<|(dom (id (cod f))),?>],<|(id (cod f)),?>] by CAT_1:58
.= [[<|(cod f),?>,<|(cod f),?>],<|(id (cod f)),?>] by CAT_1:58 ;
 dom (F . f) = <|(cod f),?> by A34, NATTRA_1:33;
hence  ( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) ) by A33, A35, A32, A36, A43, A42, FUNCT_1:2, NATTRA_1:def_17; ::_thesis: verum
end;
 for c being Object of A ex d being Object of (Functors (A,(EnsHom A))) st F . (id c) = id d
proof
let c be Object of A; ::_thesis: ex d being Object of (Functors (A,(EnsHom A))) st F . (id c) = id d
set X = dom <|(id c),?>;
 <|c,?> in Funct (A,(EnsHom A)) by CAT_2:def_2;
then reconsider d = <|c,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def_17;
take  d ; ::_thesis: F . (id c) = id d
A44: for y being set st y in dom <|(id c),?> holds
<|(id c),?> . y = (id <|c,?>) . y
proof
let y be set ; ::_thesis: ( y in dom <|(id c),?> implies <|(id c),?> . y = (id <|c,?>) . y )
assume  y in dom <|(id c),?> ; ::_thesis: <|(id c),?> . y = (id <|c,?>) . y
then reconsider z = y as Object of A by FUNCT_2:def_1;
reconsider zz = id z as Morphism of z,z ;
A45: Hom (z,z) <> {} ;
A46: <|(cod (id c)),?> is_transformable_to <|(dom (id c)),?> ;
<|(id c),?> . z = [[(Hom ((cod (id c)),z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))] by Def3
.= [[(Hom (c,z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))]
.= [[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))]
.= [[(Hom (c,z)),(Hom (c,z))],(hom (c,(id z)))] by ENS_1:53
.= [[(Hom (c,z)),(Hom (c,(cod (id z))))],(hom (c,(id z)))]
.= [[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))]
.= <|c,?> . (id z) by ENS_1:def_21
.= <|c,?> /. zz by A45, CAT_3:def_10
.= id (<|c,?> . z) by NATTRA_1:15
.= (id <|c,?>) . z by NATTRA_1:20
.= (id <|c,?>) . z by NATTRA_1:def_5 ;
hence  <|(id c),?> . y = (id <|c,?>) . y by A46, NATTRA_1:def_5; ::_thesis: verum
end;
dom <|(id c),?> = the carrier of A by FUNCT_2:def_1
.= dom (id <|c,?>) by FUNCT_2:def_1 ;
then A47: <|(id c),?> = id <|c,?> by A44, FUNCT_1:2;
F . (id c) = [[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>] by A2
.= [[<|c,?>,<|(dom (id c)),?>],<|(id c),?>] by CAT_1:58
.= [[<|c,?>,<|c,?>],(id <|c,?>)] by A47, CAT_1:58
.= id d by NATTRA_1:def_17 ;
hence  F . (id c) = id d ; ::_thesis: verum
end;
then reconsider F = F as Contravariant_Functor of A, Functors (A,(EnsHom A)) by A31, A3, OPPCAT_1:def_9;
 for f being Element of the carrier' of A holds F . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] by A2;
hence  ex b1 being Contravariant_Functor of A, Functors (A,(EnsHom A)) st
for f being Morphism of A holds b1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Contravariant_Functor of A, Functors (A,(EnsHom A)) st ( for f being Morphism of A holds b1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) & ( for f being Morphism of A holds b2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) holds
b1 = b2
proof
let h1, h2 be Contravariant_Functor of A, Functors (A,(EnsHom A)); ::_thesis: ( ( for f being Morphism of A holds h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) & ( for f being Morphism of A holds h2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) implies h1 = h2 )
assume that
A48: for f being Morphism of A holds h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] and
A49: for f being Morphism of A holds h2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ; ::_thesis: h1 = h2
now__::_thesis:_for_f_being_Morphism_of_A_holds_h1_._f_=_h2_._f
let f be Morphism of A; ::_thesis: h1 . f = h2 . f
thus h1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] by A48
.= h2 . f by A49 ; ::_thesis: verum
end;
hence  h1 = h2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Yoneda YONEDA_1:def_4_:_
 for A being Category
for b2 being Contravariant_Functor of A, Functors (A,(EnsHom A)) holds
( b2 = Yoneda A iff for f being Morphism of A holds b2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] );

definition
let A, B be Category;
let F be Contravariant_Functor of A,B;
let c be Object of A;
funcF . c ->  Object of B equals :: YONEDA_1:def 5
(Obj F) . c;
correctness
coherence
(Obj F) . c is Object of B;
;
end;

:: deftheorem  defines . YONEDA_1:def_5_:_
 for A, B being Category
for F being Contravariant_Functor of A,B
for c being Object of A holds F . c = (Obj F) . c;

theorem :: YONEDA_1:4
for A being Category
for F being Functor of A, Functors (A,(EnsHom A)) st Obj F is one-to-one & F is faithful holds
F is one-to-one
proof
let A be Category; ::_thesis: for F being Functor of A, Functors (A,(EnsHom A)) st Obj F is one-to-one & F is faithful holds
F is one-to-one
let F be Functor of A, Functors (A,(EnsHom A)); ::_thesis: ( Obj F is one-to-one & F is faithful implies F is one-to-one )
assume A1: Obj F is one-to-one ; ::_thesis: ( not F is faithful or F is one-to-one )
assume A2: F is faithful ; ::_thesis: F is one-to-one
 for x1, x2 being set st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume that
A3: ( x1 in dom F & x2 in dom F ) and
A4: F . x1 = F . x2 ; ::_thesis: x1 = x2
reconsider m1 = x1, m2 = x2 as Morphism of A by A3, FUNCT_2:def_1;
set o1 = dom m1;
set o2 = cod m1;
set o3 = dom m2;
set o4 = cod m2;
reconsider m19 = m1 as Morphism of dom m1, cod m1 by CAT_1:4;
reconsider m29 = m2 as Morphism of dom m2, cod m2 by CAT_1:4;
A5: Hom ((dom m1),(cod m1)) <> {} by CAT_1:2;
then A6: Hom ((F . (dom m1)),(F . (cod m1))) <> {} by CAT_1:84;
A7: Hom ((dom m2),(cod m2)) <> {} by CAT_1:2;
then A8: Hom ((F . (dom m2)),(F . (cod m2))) <> {} by CAT_1:84;
A9: F /. m19 = F . m2 by A4, A5, CAT_3:def_10
.= F /. m29 by A7, CAT_3:def_10 ;
(Obj F) . (dom m1) = F . (dom m1)
.= dom (F /. m29) by A9, A6, CAT_1:5
.= (Obj F) . (dom m2) by A8, CAT_1:5 ;
then A10: ( m2 is Morphism of dom m2, cod m2 & dom m1 = dom m2 ) by A1, CAT_1:4, FUNCT_2:19;
(Obj F) . (cod m1) = F . (cod m1)
.= cod (F /. m29) by A9, A6, CAT_1:5
.= (Obj F) . (cod m2) by A8, CAT_1:5 ;
then  ( m1 is Morphism of dom m1, cod m1 & m2 is Morphism of dom m1, cod m1 ) by A1, A10, CAT_1:4, FUNCT_2:19;
hence  x1 = x2 by A2, A4, A5, CAT_1:def_27; ::_thesis: verum
end;
hence  F is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;

definition
let C, D be Category;
let T be Contravariant_Functor of C,D;
attrT is faithful  means :Def6: :: YONEDA_1:def 6
 for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2;
end;

:: deftheorem Def6 defines faithful YONEDA_1:def_6_:_
 for C, D being Category
for T being Contravariant_Functor of C,D holds
( T is faithful iff for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2 );

theorem Th5: :: YONEDA_1:5
for A being Category
for F being Contravariant_Functor of A, Functors (A,(EnsHom A)) st Obj F is one-to-one & F is faithful holds
F is one-to-one
proof
let A be Category; ::_thesis: for F being Contravariant_Functor of A, Functors (A,(EnsHom A)) st Obj F is one-to-one & F is faithful holds
F is one-to-one
let F be Contravariant_Functor of A, Functors (A,(EnsHom A)); ::_thesis: ( Obj F is one-to-one & F is faithful implies F is one-to-one )
assume A1: Obj F is one-to-one ; ::_thesis: ( not F is faithful or F is one-to-one )
assume A2: F is faithful ; ::_thesis: F is one-to-one
 for x1, x2 being set st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume that
A3: ( x1 in dom F & x2 in dom F ) and
A4: F . x1 = F . x2 ; ::_thesis: x1 = x2
reconsider m1 = x1, m2 = x2 as Morphism of A by A3, FUNCT_2:def_1;
set o1 = dom m1;
set o2 = cod m1;
set o3 = dom m2;
set o4 = cod m2;
reconsider m29 = m2 as Morphism of dom m2, cod m2 by CAT_1:4;
(Obj F) . (dom m1) = cod (F . m29) by A4, OPPCAT_1:32
.= (Obj F) . (dom m2) by OPPCAT_1:32 ;
then A5: ( m2 is Morphism of dom m2, cod m2 & dom m1 = dom m2 ) by A1, CAT_1:4, FUNCT_2:19;
A6: ( m1 is Morphism of dom m1, cod m1 & Hom ((dom m1),(cod m1)) <> {} ) by CAT_1:2, CAT_1:4;
(Obj F) . (cod m1) = dom (F . m29) by A4, OPPCAT_1:32
.= (Obj F) . (cod m2) by OPPCAT_1:32 ;
then  m2 is Morphism of dom m1, cod m1 by A1, A5, FUNCT_2:19;
hence  x1 = x2 by A2, A4, A6, Def6; ::_thesis: verum
end;
hence  F is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;

registration
let A be Category;
cluster Yoneda A ->  faithful ;
coherence
 Yoneda A is faithful
proof
set F = Yoneda A;
 for o1, o2 being Object of A st Hom (o1,o2) <> {} holds
for x1, x2 being Morphism of o1,o2 st (Yoneda A) . x1 = (Yoneda A) . x2 holds
x1 = x2
proof
let o1, o2 be Object of A; ::_thesis: ( Hom (o1,o2) <> {} implies for x1, x2 being Morphism of o1,o2 st (Yoneda A) . x1 = (Yoneda A) . x2 holds
x1 = x2 )
assume A1: Hom (o1,o2) <> {} ; ::_thesis: for x1, x2 being Morphism of o1,o2 st (Yoneda A) . x1 = (Yoneda A) . x2 holds
x1 = x2
let x1, x2 be Morphism of o1,o2; ::_thesis: ( (Yoneda A) . x1 = (Yoneda A) . x2 implies x1 = x2 )
A2: x2 in Hom (o1,o2) by A1, CAT_1:def_5;
assume  (Yoneda A) . x1 = (Yoneda A) . x2 ; ::_thesis: x1 = x2
then  [[<|(cod x1),?>,<|(dom x1),?>],<|x1,?>] = (Yoneda A) . x2 by Def4;
then  [[<|(cod x1),?>,<|(dom x1),?>],<|x1,?>] = [[<|(cod x2),?>,<|(dom x2),?>],<|x2,?>] by Def4;
then  [<|(cod x1),?>,<|(dom x1),?>,<|x1,?>] = [[<|(cod x2),?>,<|(dom x2),?>],<|x2,?>] ;
then  [<|(cod x1),?>,<|(dom x1),?>,<|x1,?>] = [<|(cod x2),?>,<|(dom x2),?>,<|x2,?>] ;
then A3: <|x1,?> = <|x2,?> by XTUPLE_0:3;
A4: x1 in Hom (o1,o2) by A1, CAT_1:def_5;
then A5: dom x1 = o1 by CAT_1:1
.= dom x2 by A2, CAT_1:1 ;
cod x1 = o2 by A4, CAT_1:1
.= cod x2 by A2, CAT_1:1 ;
then  [[(Hom ((cod x1),o2)),(Hom ((dom x1),o2))],(hom (x1,(id o2)))] = <|x2,?> . o2 by A5, A3, Def3;
then  [[(Hom ((cod x1),o2)),(Hom ((dom x1),o2))],(hom (x1,(id o2)))] = [[(Hom ((cod x2),o2)),(Hom ((dom x2),o2))],(hom (x2,(id o2)))] by Def3;
then  [[(Hom (o2,o2)),(Hom ((dom x1),o2))],(hom (x1,(id o2)))] = [[(Hom ((cod x2),o2)),(Hom ((dom x2),o2))],(hom (x2,(id o2)))] by A4, CAT_1:1;
then  [[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x1,(id o2)))] = [[(Hom ((cod x2),o2)),(Hom ((dom x2),o2))],(hom (x2,(id o2)))] by A4, CAT_1:1;
then  [[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x1,(id o2)))] = [[(Hom (o2,o2)),(Hom ((dom x2),o2))],(hom (x2,(id o2)))] by A2, CAT_1:1;
then  [[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x1,(id o2)))] = [[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x2,(id o2)))] by A2, CAT_1:1;
then  [[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x1,(id o2)))] = [(Hom (o2,o2)),(Hom (o1,o2)),(hom (x2,(id o2)))] ;
then A6: [(Hom (o2,o2)),(Hom (o1,o2)),(hom (x1,(id o2)))] = [(Hom (o2,o2)),(Hom (o1,o2)),(hom (x2,(id o2)))] ;
reconsider dd = id o2 as Morphism of A ;
A7: Hom (o2,o2) <> {} ;
then A8: (id o2) (*) dd = (id o2) * (id o2) by CAT_1:def_13;
 id o2 in Hom (o2,o2) by CAT_1:27;
then  id o2 in Hom ((cod x2),o2) by A2, CAT_1:1;
then  id o2 in Hom ((cod x2),(dom (id o2))) ;
then A9: (hom (x2,(id o2))) . dd = ((id o2) * (id o2)) (*) x2 by A8, ENS_1:def_23
.= (id o2) (*) x2
.= (id o2) * x2 by A1, A7, CAT_1:def_13
.= x2 by A1, CAT_1:28 ;
 id o2 in Hom (o2,o2) by CAT_1:27;
then  id o2 in Hom ((cod x1),o2) by A4, CAT_1:1;
then  id o2 in Hom ((cod x1),(dom (id o2))) ;
then (hom (x1,(id o2))) . dd = ((id o2) * (id o2)) (*) x1 by A8, ENS_1:def_23
.= (id o2) (*) x1
.= (id o2) * x1 by A1, A7, CAT_1:def_13
.= x1 by A1, CAT_1:28 ;
hence  x1 = x2 by A9, A6, XTUPLE_0:3; ::_thesis: verum
end;
hence  Yoneda A is faithful by Def6; ::_thesis: verum
end;
end;

registration
let A be Category;
cluster Yoneda A ->  one-to-one ;
coherence
 Yoneda A is one-to-one
proof
set F = Yoneda A;
 for x1, x2 being set st x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) & (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) & (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 implies x1 = x2 )
assume that
A1: ( x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) ) and
A2: (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 ; ::_thesis: x1 = x2
reconsider c = x1, c1 = x2 as Object of A by A1, FUNCT_2:def_1;
reconsider f = id c1 as Morphism of c1,c1 ;
A3: Hom (c1,c1) <> {} ;
 <|c1,?> in Funct (A,(EnsHom A)) by CAT_2:def_2;
then reconsider d1 = <|c1,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def_17;
 <|c,?> in Funct (A,(EnsHom A)) by CAT_2:def_2;
then reconsider d = <|c,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def_17;
 (Yoneda A) . (id c1) = id d1
proof
set X = dom <|(id c1),?>;
A4: for y being set st y in dom <|(id c1),?> holds
<|(id c1),?> . y = (id <|c1,?>) . y
proof
let y be set ; ::_thesis: ( y in dom <|(id c1),?> implies <|(id c1),?> . y = (id <|c1,?>) . y )
assume  y in dom <|(id c1),?> ; ::_thesis: <|(id c1),?> . y = (id <|c1,?>) . y
then reconsider z = y as Object of A by FUNCT_2:def_1;
reconsider zz = id z as Morphism of z,z ;
A5: Hom (z,z) <> {} ;
A6: <|(cod (id c1)),?> is_transformable_to <|(dom (id c1)),?> ;
<|(id c1),?> . z = [[(Hom ((cod (id c1)),z)),(Hom ((dom (id c1)),z))],(hom ((id c1),(id z)))] by Def3
.= [[(Hom (c1,z)),(Hom ((dom (id c1)),z))],(hom ((id c1),(id z)))]
.= [[(Hom (c1,z)),(Hom (c1,z))],(hom ((id c1),(id z)))]
.= [[(Hom (c1,z)),(Hom (c1,z))],(hom (c1,(id z)))] by ENS_1:53
.= [[(Hom (c1,z)),(Hom (c1,(cod (id z))))],(hom (c1,(id z)))]
.= [[(Hom (c1,(dom (id z)))),(Hom (c1,(cod (id z))))],(hom (c1,(id z)))]
.= <|c1,?> . (id z) by ENS_1:def_21
.= <|c1,?> /. zz by A5, CAT_3:def_10
.= id (<|c1,?> . z) by NATTRA_1:15
.= (id <|c1,?>) . z by NATTRA_1:20
.= (id <|c1,?>) . z by NATTRA_1:def_5 ;
hence  <|(id c1),?> . y = (id <|c1,?>) . y by A6, NATTRA_1:def_5; ::_thesis: verum
end;
dom <|(id c1),?> = the carrier of A by FUNCT_2:def_1
.= dom (id <|c1,?>) by FUNCT_2:def_1 ;
then A7: <|(id c1),?> = id <|c1,?> by A4, FUNCT_1:2;
(Yoneda A) . (id c1) = [[<|(cod (id c1)),?>,<|(dom (id c1)),?>],<|(id c1),?>] by Def4
.= [[<|c1,?>,<|(dom (id c1)),?>],<|(id c1),?>] by CAT_1:58
.= [[<|c1,?>,<|c1,?>],(id <|c1,?>)] by A7, CAT_1:58
.= id d1 by NATTRA_1:def_17 ;
hence  (Yoneda A) . (id c1) = id d1 ; ::_thesis: verum
end;
then A8: (Obj (Yoneda A)) . c1 = d1 by OPPCAT_1:30;
 (Yoneda A) . (id c) = id d
proof
set X = dom <|(id c),?>;
A9: for y being set st y in dom <|(id c),?> holds
<|(id c),?> . y = (id <|c,?>) . y
proof
let y be set ; ::_thesis: ( y in dom <|(id c),?> implies <|(id c),?> . y = (id <|c,?>) . y )
assume  y in dom <|(id c),?> ; ::_thesis: <|(id c),?> . y = (id <|c,?>) . y
then reconsider z = y as Object of A by FUNCT_2:def_1;
reconsider zz = id z as Morphism of z,z ;
A10: Hom (z,z) <> {} ;
A11: <|(cod (id c)),?> is_transformable_to <|(dom (id c)),?> ;
<|(id c),?> . z = [[(Hom ((cod (id c)),z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))] by Def3
.= [[(Hom (c,z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))]
.= [[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))]
.= [[(Hom (c,z)),(Hom (c,z))],(hom (c,(id z)))] by ENS_1:53
.= [[(Hom (c,z)),(Hom (c,(cod (id z))))],(hom (c,(id z)))]
.= [[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))]
.= <|c,?> . (id z) by ENS_1:def_21
.= <|c,?> /. zz by A10, CAT_3:def_10
.= id (<|c,?> . z) by NATTRA_1:15
.= (id <|c,?>) . z by NATTRA_1:20
.= (id <|c,?>) . z by NATTRA_1:def_5 ;
hence  <|(id c),?> . y = (id <|c,?>) . y by A11, NATTRA_1:def_5; ::_thesis: verum
end;
dom <|(id c),?> = the carrier of A by FUNCT_2:def_1
.= dom (id <|c,?>) by FUNCT_2:def_1 ;
then A12: <|(id c),?> = id <|c,?> by A9, FUNCT_1:2;
(Yoneda A) . (id c) = [[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>] by Def4
.= [[<|c,?>,<|(dom (id c)),?>],<|(id c),?>] by CAT_1:58
.= [[<|c,?>,<|c,?>],(id <|c,?>)] by A12, CAT_1:58
.= id d by NATTRA_1:def_17 ;
hence  (Yoneda A) . (id c) = id d ; ::_thesis: verum
end;
then  (Obj (Yoneda A)) . c = d by OPPCAT_1:30;
then  [[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = (hom?- c1) . f by A2, A8, ENS_1:def_21;
then  [[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))] by ENS_1:def_21;
then  [(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))] ;
then  [(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [(Hom (c1,(dom f))),(Hom (c1,(cod f))),(hom (c1,f))] ;
then  Hom (c,(dom f)) = Hom (c1,(dom f)) by XTUPLE_0:3;
then  Hom (c,(dom f)) = Hom (c1,c1) by CAT_1:5;
then A13: Hom (c,c1) = Hom (c1,c1) by CAT_1:5;
 id c1 in Hom (c1,c1) by CAT_1:27;
then reconsider h = id c1 as Morphism of c,c1 by A13, CAT_1:def_5;
 dom h = c by A13, CAT_1:5;
hence  x1 = x2 by A3, CAT_1:5; ::_thesis: verum
end;
then  Obj (Yoneda A) is one-to-one by FUNCT_1:def_4;
hence  Yoneda A is one-to-one by Th5; ::_thesis: verum
end;
end;

definition
let C, D be Category;
let T be Contravariant_Functor of C,D;
attrT is full  means :Def7: :: YONEDA_1:def 7
 for c, c9 being Object of C st Hom ((T . c9),(T . c)) <> {} holds
for g being Morphism of T . c9,T . c holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f );
end;

:: deftheorem Def7 defines full YONEDA_1:def_7_:_
 for C, D being Category
for T being Contravariant_Functor of C,D holds
( T is full iff for c, c9 being Object of C st Hom ((T . c9),(T . c)) <> {} holds
for g being Morphism of T . c9,T . c holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) );

registration
let A be Category;
cluster Yoneda A ->  full ;
coherence
 Yoneda A is full
proof
set F = Yoneda A;
 for c, c9 being Object of A st Hom (((Yoneda A) . c9),((Yoneda A) . c)) <> {} holds
for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f )
proof
let c, c9 be Object of A; ::_thesis: ( Hom (((Yoneda A) . c9),((Yoneda A) . c)) <> {} implies for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f ) )
assume A1: Hom (((Yoneda A) . c9),((Yoneda A) . c)) <> {} ; ::_thesis: for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f )
A2: <|c9,?> . c9 = (hom?- ((Hom A),c9)) . c9 by ENS_1:def_25
.= (Obj (hom?- ((Hom A),c9))) . c9
.= Hom (c9,c9) by ENS_1:60 ;
let g be Morphism of (Yoneda A) . c9,(Yoneda A) . c; ::_thesis: ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f )
 g in the carrier' of (Functors (A,(EnsHom A))) ;
then  g in NatTrans (A,(EnsHom A)) by NATTRA_1:def_17;
then consider F1, F2 being Functor of A, EnsHom A, t being natural_transformation of F1,F2 such that
A3: g = [[F1,F2],t] and
A4: F1 is_naturally_transformable_to F2 by NATTRA_1:def_16;
A5: dom g = F1 by A3, NATTRA_1:33;
 <|c9,?> in Funct (A,(EnsHom A)) by CAT_2:def_2;
then reconsider d1 = <|c9,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def_17;
 <|c,?> in Funct (A,(EnsHom A)) by CAT_2:def_2;
then reconsider d = <|c,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def_17;
A6: (Yoneda A) . (id c) = id d
proof
set X = dom <|(id c),?>;
A7: for y being set st y in dom <|(id c),?> holds
<|(id c),?> . y = (id <|c,?>) . y
proof
let y be set ; ::_thesis: ( y in dom <|(id c),?> implies <|(id c),?> . y = (id <|c,?>) . y )
assume  y in dom <|(id c),?> ; ::_thesis: <|(id c),?> . y = (id <|c,?>) . y
then reconsider z = y as Object of A by FUNCT_2:def_1;
reconsider zz = id z as Morphism of z,z ;
A8: Hom (z,z) <> {} ;
A9: <|(cod (id c)),?> is_transformable_to <|(dom (id c)),?> ;
<|(id c),?> . z = [[(Hom ((cod (id c)),z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))] by Def3
.= [[(Hom (c,z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))]
.= [[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))]
.= [[(Hom (c,z)),(Hom (c,z))],(hom (c,(id z)))] by ENS_1:53
.= [[(Hom (c,z)),(Hom (c,(cod (id z))))],(hom (c,(id z)))]
.= [[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))]
.= <|c,?> . (id z) by ENS_1:def_21
.= <|c,?> /. zz by A8, CAT_3:def_10
.= id (<|c,?> . z) by NATTRA_1:15
.= (id <|c,?>) . z by NATTRA_1:20
.= (id <|c,?>) . z by NATTRA_1:def_5 ;
hence  <|(id c),?> . y = (id <|c,?>) . y by A9, NATTRA_1:def_5; ::_thesis: verum
end;
dom <|(id c),?> = the carrier of A by FUNCT_2:def_1
.= dom (id <|c,?>) by FUNCT_2:def_1 ;
then A10: <|(id c),?> = id <|c,?> by A7, FUNCT_1:2;
(Yoneda A) . (id c) = [[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>] by Def4
.= [[<|c,?>,<|(dom (id c)),?>],<|(id c),?>] by CAT_1:58
.= [[<|c,?>,<|c,?>],(id <|c,?>)] by A10, CAT_1:58
.= id d by NATTRA_1:def_17 ;
hence  (Yoneda A) . (id c) = id d ; ::_thesis: verum
end;
then A11: (Yoneda A) . c = d by OPPCAT_1:30;
A12: (Yoneda A) . (id c9) = id d1
proof
set X = dom <|(id c9),?>;
A13: for y being set st y in dom <|(id c9),?> holds
<|(id c9),?> . y = (id <|c9,?>) . y
proof
let y be set ; ::_thesis: ( y in dom <|(id c9),?> implies <|(id c9),?> . y = (id <|c9,?>) . y )
assume  y in dom <|(id c9),?> ; ::_thesis: <|(id c9),?> . y = (id <|c9,?>) . y
then reconsider z = y as Object of A by FUNCT_2:def_1;
reconsider zz = id z as Morphism of z,z ;
A14: Hom (z,z) <> {} ;
A15: <|(cod (id c9)),?> is_transformable_to <|(dom (id c9)),?> ;
<|(id c9),?> . z = [[(Hom ((cod (id c9)),z)),(Hom ((dom (id c9)),z))],(hom ((id c9),(id z)))] by Def3
.= [[(Hom (c9,z)),(Hom ((dom (id c9)),z))],(hom ((id c9),(id z)))]
.= [[(Hom (c9,z)),(Hom (c9,z))],(hom ((id c9),(id z)))]
.= [[(Hom (c9,z)),(Hom (c9,z))],(hom (c9,(id z)))] by ENS_1:53
.= [[(Hom (c9,z)),(Hom (c9,(cod (id z))))],(hom (c9,(id z)))]
.= [[(Hom (c9,(dom (id z)))),(Hom (c9,(cod (id z))))],(hom (c9,(id z)))]
.= <|c9,?> . (id z) by ENS_1:def_21
.= <|c9,?> /. zz by A14, CAT_3:def_10
.= id (<|c9,?> . z) by NATTRA_1:15
.= (id <|c9,?>) . z by NATTRA_1:20
.= (id <|c9,?>) . z by NATTRA_1:def_5 ;
hence  <|(id c9),?> . y = (id <|c9,?>) . y by A15, NATTRA_1:def_5; ::_thesis: verum
end;
dom <|(id c9),?> = the carrier of A by FUNCT_2:def_1
.= dom (id <|c9,?>) by FUNCT_2:def_1 ;
then A16: <|(id c9),?> = id <|c9,?> by A13, FUNCT_1:2;
(Yoneda A) . (id c9) = [[<|(cod (id c9)),?>,<|(dom (id c9)),?>],<|(id c9),?>] by Def4
.= [[<|c9,?>,<|(dom (id c9)),?>],<|(id c9),?>] by CAT_1:58
.= [[<|c9,?>,<|c9,?>],(id <|c9,?>)] by A16, CAT_1:58
.= id d1 by NATTRA_1:def_17 ;
hence  (Yoneda A) . (id c9) = id d1 ; ::_thesis: verum
end;
then A17: (Obj (Yoneda A)) . c9 = d1 by OPPCAT_1:30;
A18: cod g = F2 by A3, NATTRA_1:33;
then A19: F2 = (Yoneda A) . c by A1, CAT_1:5;
A20: (Yoneda A) . c9 = d1 by A12, OPPCAT_1:30;
A21: <|c,?> . c9 = (hom?- ((Hom A),c)) . c9 by ENS_1:def_25
.= (Obj (hom?- ((Hom A),c))) . c9
.= Hom (c,c9) by ENS_1:60 ;
A22: ( dom g = (Yoneda A) . c9 & cod g = (Yoneda A) . c ) by A1, CAT_1:5;
then reconsider t = t as natural_transformation of <|c9,?>,<|c,?> by A5, A18, A12, A11, OPPCAT_1:30;
 (Obj (Yoneda A)) . c = d by A6, OPPCAT_1:30;
then  <|c9,?> is_transformable_to <|c,?> by A4, A5, A18, A22, A20, NATTRA_1:def_7;
then  Hom ((<|c9,?> . c9),(<|c,?> . c9)) <> {} by NATTRA_1:def_2;
then A23: t . c9 in Hom ((<|c9,?> . c9),(<|c,?> . c9)) by CAT_1:def_5;
then A24: cod (t . c9) = <|c,?> . c9 by CAT_1:1;
A25: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def_13;
then reconsider t1 = t . c9 as Element of Maps (Hom A) ;
A26: cod (t . c9) = (fCod (Hom A)) . (t . c9) by A25
.= cod t1 by ENS_1:def_10 ;
 t1 in Maps ((dom t1),(cod t1)) by ENS_1:19;
then A27: t1 `2 in Funcs ((dom t1),(cod t1)) by ENS_1:20;
A28: dom (t . c9) = <|c9,?> . c9 by A23, CAT_1:1;
then  the Source of (EnsHom A) . (t . c9) <> {} by A2;
then  dom t1 <> {} by A25, ENS_1:def_9;
then A29: cod t1 <> {} by A27;
then A30: cod (t . c9) <> {} by A25, ENS_1:def_10;
hence  Hom (c,c9) <> {} by A21, A23, CAT_1:1; ::_thesis: ex f being Morphism of c,c9 st g = (Yoneda A) . f
dom (t . c9) = (fDom (Hom A)) . (t . c9) by A25
.= dom t1 by ENS_1:def_9 ;
then A31: t1 `2 is Function of (<|c9,?> . c9),(<|c,?> . c9) by A28, A24, A27, A26, FUNCT_2:66;
then A32: dom (t1 `2) = Hom (c9,c9) by A2, A24, A30, FUNCT_2:def_1;
then  id c9 in dom (t1 `2) by CAT_1:27;
then A33: (t1 `2) . (id c9) in rng (t1 `2) by FUNCT_1:def_3;
 rng (t1 `2) c= Hom (c,c9) by A21, A31, RELAT_1:def_19;
then  (t1 `2) . (id c9) in Hom (c,c9) by A33;
then reconsider f = (t1 `2) . (id c9) as Morphism of c,c9 by CAT_1:def_5;
A34: <|c,?> . c9 <> {} by A24, A25, A29, ENS_1:def_10;
then A35: dom f = c by A21, CAT_1:5;
take  f ; ::_thesis: g = (Yoneda A) . f
A36: cod f = c9 by A21, A34, CAT_1:5;
A37: F1 = (Yoneda A) . c9 by A1, A5, CAT_1:5;
then A38: <|c9,?> is_transformable_to <|c,?> by A4, A19, A17, A11, NATTRA_1:def_7;
 for a being Object of A holds <|f,?> . a = t . a
proof
let a be Object of A; ::_thesis: <|f,?> . a = t . a
A39: <|c,?> . a = (hom?- ((Hom A),c)) . a by ENS_1:def_25
.= (Obj (hom?- ((Hom A),c))) . a
.= Hom (c,a) by ENS_1:60 ;
reconsider ta1 = t . a as Element of Maps (Hom A) by A25;
A40: <|c9,?> . a = (hom?- ((Hom A),c9)) . a by ENS_1:def_25
.= (Obj (hom?- ((Hom A),c9))) . a
.= Hom (c9,a) by ENS_1:60 ;
 ta1 in Maps ((dom ta1),(cod ta1)) by ENS_1:19;
then A41: ta1 `2 in Funcs ((dom ta1),(cod ta1)) by ENS_1:20;
then A42: ta1 `2 is Function of (dom ta1),(cod ta1) by FUNCT_2:66;
set X = dom (ta1 `2);
A43: dom (t . a) = (fDom (Hom A)) . (t . a) by A25
.= dom ta1 by ENS_1:def_9 ;
A44: Hom ((<|c9,?> . a),(<|c,?> . a)) <> {} by A38, NATTRA_1:def_2;
then A45: dom (t . a) = <|c9,?> . a by CAT_1:5;
A46: cod (t . a) = <|c,?> . a by A44, CAT_1:5;
A47: cod (t . a) = (fCod (Hom A)) . (t . a) by A25
.= cod ta1 by ENS_1:def_10 ;
then A48: ta1 = [[(<|c9,?> . a),(<|c,?> . a)],(ta1 `2)] by A45, A46, A43, ENS_1:8;
A49: ta1 `2 is Function of (dom (t . a)),(cod (t . a)) by A43, A47, A41, FUNCT_2:66;
A50: dom (ta1 `2) = Hom (c9,a)
proof
percases ( Hom (c9,a) = {} or Hom (c9,a) <> {} ) ;
suppose Hom (c9,a) = {} ; ::_thesis: dom (ta1 `2) = Hom (c9,a)
hence  dom (ta1 `2) = Hom (c9,a) by A45, A43, A40, A42; ::_thesis: verum
end;
suppose Hom (c9,a) <> {} ; ::_thesis: dom (ta1 `2) = Hom (c9,a)
then  Hom ((dom f),a) <> {} by A36, ENS_1:42;
hence  dom (ta1 `2) = Hom (c9,a) by A35, A45, A46, A40, A39, A49, FUNCT_2:def_1; ::_thesis: verum
end;
end;
end;
A51: for x being set st x in dom (ta1 `2) holds
(hom (f,(id a))) . x = (ta1 `2) . x
proof
reconsider t1 = t . c9 as Element of Maps (Hom A) by A25;
let x be set ; ::_thesis: ( x in dom (ta1 `2) implies (hom (f,(id a))) . x = (ta1 `2) . x )
A52: f in Hom (c,(cod f)) by A35;
assume A53: x in dom (ta1 `2) ; ::_thesis: (hom (f,(id a))) . x = (ta1 `2) . x
then reconsider y = x as Morphism of cod f,a by A36, A50, CAT_1:def_5;
reconsider h = y as Morphism of c9,a by A21, A24, A30, CAT_1:5;
A54: dom h = c9 by A50, A53, CAT_1:5;
reconsider tc9 = <|c9,?> . h as Element of Maps (Hom A) by A25;
A55: cod h = a by A50, A53, CAT_1:5;
reconsider tch = <|c,?> . h as Element of Maps (Hom A) by A25;
A56: [[(Hom (c,(dom h))),(Hom (c,(cod h)))],(hom (c,h))] = <|c,?> . h by ENS_1:def_21
.= <|c,?> . h ;
A57: [[(Hom (c9,(dom h))),(Hom (c9,(cod h)))],(hom (c9,h))] = <|c9,?> . h by ENS_1:def_21
.= <|c9,?> . h ;
A58: cod (<|c9,?> . h) = (fCod (Hom A)) . (<|c9,?> . h) by A25
.= cod tc9 by ENS_1:def_10 ;
then A59: cod (<|c9,?> . h) = (tc9 `1) `2 by ENS_1:def_4
.= [(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `2 by A57, MCART_1:7
.= Hom (c9,(cod h)) ;
then A60: [(t . a),(<|c9,?> . h)] in dom the Comp of (EnsHom A) by A45, A40, A55, CAT_1:15;
 tc9 in Maps ((dom tc9),(cod tc9)) by ENS_1:19;
then A61: tc9 `2 in Funcs ((dom tc9),(cod tc9)) by ENS_1:20;
A62: dom (<|c9,?> . h) = (fDom (Hom A)) . (<|c9,?> . h) by A25
.= dom tc9 by ENS_1:def_9 ;
then  dom (<|c9,?> . h) = (tc9 `1) `1 by ENS_1:def_3
.= [(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `1 by A57, MCART_1:7
.= Hom (c9,(dom h)) ;
then  tc9 `2 is Function of (Hom (c9,(dom h))),(Hom (c9,(cod h))) by A62, A58, A59, A61, FUNCT_2:66;
then A63: dom (tc9 `2) = Hom (c9,c9) by A50, A53, A54, A55, FUNCT_2:def_1;
A64: dom y = cod f by A36, A50, A53, CAT_1:5;
 tch = [[(dom tch),(cod tch)],(tch `2)] by ENS_1:8;
then  [(Hom (c,(dom h))),(Hom (c,(cod h))),(hom (c,h))] = [[(dom tch),(cod tch)],(tch `2)] by A56;
then  [(Hom (c,(dom h))),(Hom (c,(cod h))),(hom (c,h))] = [(dom tch),(cod tch),(tch `2)] ;
then A65: hom (c,h) = tch `2 by XTUPLE_0:3;
 tc9 = [[(dom tc9),(cod tc9)],(tc9 `2)] by ENS_1:8;
then  [(dom tc9),(cod tc9),(tc9 `2)] = [[(Hom (c9,(dom h))),(Hom (c9,(cod h)))],(hom (c9,h))] by A57;
then  [(dom tc9),(cod tc9),(tc9 `2)] = [(Hom (c9,(dom h))),(Hom (c9,(cod h))),(hom (c9,h))] ;
then A66: tc9 `2 = hom (c9,h) by XTUPLE_0:3;
A67: Hom ((<|c9,?> . c9),(<|c,?> . c9)) <> {} by A38, NATTRA_1:def_2;
then  t . c9 in Hom ((<|c9,?> . c9),(<|c,?> . c9)) by CAT_1:def_5;
then A68: cod (t . c9) = <|c,?> . c9 by CAT_1:1;
dom (<|c,?> . h) = (fDom (Hom A)) . (<|c,?> . h) by A25
.= dom tch by ENS_1:def_9 ;
then  dom (<|c,?> . h) = (tch `1) `1 by ENS_1:def_3
.= [(Hom (c,(dom h))),(Hom (c,(cod h)))] `1 by A56, MCART_1:7
.= Hom (c,(dom h)) ;
then A69: [(<|c,?> . h),(t . c9)] in dom the Comp of (EnsHom A) by A21, A54, A68, CAT_1:15;
cod (t . c9) = (fCod (Hom A)) . (t . c9) by A25
.= cod t1 by ENS_1:def_10 ;
then A70: cod t1 = [(Hom (c,(dom h))),(Hom (c,(cod h)))] `1 by A21, A54, A68
.= (tch `1) `1 by A56, MCART_1:7
.= dom tch by ENS_1:def_3 ;
A71: h in Hom (c9,a) by A50, A53;
then A72: <|c,?> /. h = <|c,?> . h by CAT_3:def_10;
 Hom ((<|c,?> . c9),(<|c,?> . a)) <> {} by A50, A53, CAT_1:84;
then A73: (<|c,?> /. h) * (t . c9) = (<|c,?> . h) (*) (t . c9) by A67, A72, CAT_1:def_13
.= (fComp (Hom A)) . (tch,t1) by A25, A69, CAT_1:def_1
.= tch * t1 by A70, ENS_1:def_11
.= [[(dom t1),(cod tch)],((tch `2) * (t1 `2))] by A70, ENS_1:def_6 ;
A74: cod tc9 = (tc9 `1) `2 by ENS_1:def_4
.= [(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `2 by A57, MCART_1:7
.= dom ta1 by A45, A43, A40, A55 ;
A75: <|c9,?> /. h = <|c9,?> . h by A71, CAT_3:def_10;
 Hom ((<|c9,?> . c9),(<|c9,?> . a)) <> {} by A50, A53, CAT_1:84;
then A76: (t . a) * (<|c9,?> /. h) = (t . a) (*) (<|c9,?> . h) by A44, A75, CAT_1:def_13
.= (fComp (Hom A)) . (ta1,tc9) by A25, A60, CAT_1:def_1
.= ta1 * tc9 by A74, ENS_1:def_11
.= [[(dom tc9),(cod ta1)],((ta1 `2) * (tc9 `2))] by A74, ENS_1:def_6 ;
 (t . a) * (<|c9,?> /. h) = (<|c,?> /. h) * (t . c9) by A4, A37, A19, A17, A11, A50, A53, NATTRA_1:def_8;
then  [(dom tc9),(cod ta1),((ta1 `2) * (tc9 `2))] = [[(dom t1),(cod tch)],((tch `2) * (t1 `2))] by A76, A73;
then  [(dom tc9),(cod ta1),((ta1 `2) * (tc9 `2))] = [(dom t1),(cod tch),((tch `2) * (t1 `2))] ;
then A77: (ta1 `2) * (tc9 `2) = (tch `2) * (t1 `2) by XTUPLE_0:3;
A78: id c9 in Hom (c9,(cod f)) by A36, CAT_1:27;
(hom (f,(id a))) . x = (hom (f,a)) . y by ENS_1:53
.= y (*) f by A36, A50, A53, ENS_1:def_20
.= (tch `2) . ((t1 `2) . (id c9)) by A64, A65, A52, ENS_1:def_19
.= ((ta1 `2) * (tc9 `2)) . (id c9) by A32, A77, CAT_1:27, FUNCT_1:13
.= (ta1 `2) . ((hom (c9,h)) . (id c9)) by A66, A63, CAT_1:27, FUNCT_1:13
.= (ta1 `2) . (y (*) (id c9)) by A64, A78, ENS_1:def_19
.= (ta1 `2) . x by A36, A64, CAT_1:22 ;
hence  (hom (f,(id a))) . x = (ta1 `2) . x ; ::_thesis: verum
end;
 dom (hom (f,a)) = Hom ((cod f),a)
proof
percases ( Hom ((cod f),a) = {} or Hom ((cod f),a) <> {} ) ;
suppose Hom ((cod f),a) = {} ; ::_thesis: dom (hom (f,a)) = Hom ((cod f),a)
hence  dom (hom (f,a)) = Hom ((cod f),a) ; ::_thesis: verum
end;
suppose Hom ((cod f),a) <> {} ; ::_thesis: dom (hom (f,a)) = Hom ((cod f),a)
then  Hom (c,a) <> {} by A35, ENS_1:42;
hence  dom (hom (f,a)) = Hom ((cod f),a) by A35, FUNCT_2:def_1; ::_thesis: verum
end;
end;
end;
then  dom (ta1 `2) = dom (hom (f,(id a))) by A36, A50, ENS_1:53;
then  hom (f,(id a)) = ta1 `2 by A51, FUNCT_1:2;
hence  <|f,?> . a = t . a by A35, A36, A40, A39, A48, Def3; ::_thesis: verum
end;
then  <|f,?> = t by A4, A37, A19, A17, A11, A35, A36, ISOCAT_1:26;
hence  g = (Yoneda A) . f by A3, A5, A18, A22, A17, A11, A35, A36, Def4; ::_thesis: verum
end;
hence  Yoneda A is full by Def7; ::_thesis: verum
end;
end;