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 H₁( 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)),(fId (Hom A)) #) by ENS_1:def 14;
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 11
.= (m `1 ) `2 by ENS_1:def 5
.= [(Hom (cod f),a),(Hom (dom f),a)] `2 by MCART_1:7
.= Hom (dom f),a by MCART_1:7
.= (Obj (hom?- (Hom A),(dom f))) . a by ENS_1:60
.= (hom?- (Hom A),(dom f)) . a by CAT_1:def 20
.= <|(dom f),?> . a by ENS_1:def 26 ;
dom m = (fDom (Hom A)) . m by A2
.= dom m9 by ENS_1:def 10
.= (m `1 ) `1 by ENS_1:def 4
.= [(Hom (cod f),a),(Hom (dom f),a)] `1 by MCART_1:7
.= Hom (cod f),a by MCART_1:7
.= (Obj (hom?- (Hom A),(cod f))) . a by ENS_1:60
.= (hom?- (Hom A),(cod f)) . a by CAT_1:def 20
.= <|(cod f),?> . a by ENS_1:def 26 ;
hence [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] in Hom (<|(cod f),?> . a),(<|(dom f),?> . a) by A3, CAT_1:18; :: thesis: verum

end;

A4: for a being Element of A holds H₁(a) in the carrier' of (EnsHom A)

proof

let a be Object of A; :: thesis: H₁(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 H₁(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 = H₁(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 7;
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:126;
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:23;
A11: rng (hom (cod f),g) c= dom (hom f,b)

proof

A12: cod g = b by A8, CAT_1:23;

per cases ( Hom (dom f),b = {} or Hom (dom f),b <> {} ) ;

suppose A13: Hom (dom f),b = {} ; :: thesis: rng (hom (cod f),g) c= dom (hom f,b)

A14: rng (hom (cod f),g) c= Hom (cod f),(cod g) by RELAT_1:def 19;
Hom (cod f),b = {} by A13, ENS_1:42;
hence rng (hom (cod f),g) c= dom (hom f,b) by A12, A14, FUNCT_2:def 1; :: thesis: verum

end;

suppose A15: Hom (dom f),b <> {} ; :: thesis: rng (hom (cod f),g) c= dom (hom f,b)

cod g = b by A8, CAT_1:23;
then A16: ( rng (hom (cod f),g) c= Hom (cod f),(cod g) & Hom (cod f),(cod g) = dom (hom f,b) ) by A15, 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 A16; :: thesis: verum

end;

end;

end;

A17: rng (hom f,a) c= dom (hom (dom f),g)

proof

A18: dom g = a by A8, CAT_1:23;

per cases ( Hom (dom f),(cod g) = {} or Hom (dom f),(cod g) <> {} ) ;

suppose A19: Hom (dom f),(cod g) = {} ; :: thesis: rng (hom f,a) c= dom (hom (dom f),g)

A20: rng (hom f,a) c= Hom (dom f),a by RELAT_1:def 19;
Hom (dom f),(dom g) = {} by A19, ENS_1:42;
hence rng (hom f,a) c= dom (hom (dom f),g) by A18, A20, FUNCT_2:def 1; :: thesis: verum

end;

suppose A21: 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 A18, 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

per cases ( Hom (cod f),(dom g) = {} or Hom (cod f),(dom g) <> {} ) ;

suppose A24: 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:46
.= Hom (cod f),(dom g) by A24, FUNCT_2:def 1
.= dom (hom f,a) by A10, A24, FUNCT_2:def 1
.= dom ((hom (dom f),g) * (hom f,a)) by A17, RELAT_1:46 ;
hence dom ((hom f,b) * (hom (cod f),g)) = dom ((hom (dom f),g) * (hom f,a)) ; :: thesis: verum

end;

suppose A25: 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 A10, A25, ENS_1:42;
dom ((hom f,b) * (hom (cod f),g)) = dom (hom (cod f),g) by A11, RELAT_1:46
.= Hom (cod f),(dom g) by A26, FUNCT_2:def 1
.= Hom (cod f),a by A8, CAT_1:23
.= dom (hom f,a) by A27, FUNCT_2:def 1
.= dom ((hom (dom f),g) * (hom f,a)) by A17, RELAT_1:46 ;
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

per cases ( Hom (cod f),(dom g) <> {} or Hom (cod f),(dom g) = {} ) ;

suppose A30: 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:21;
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 & dom x = cod f ) by A32, CAT_1:18;
A34: dom g = cod x by A32, CAT_1:18;
then A35: cod (g * x) = cod g by CAT_1:42
.= b by A8, CAT_1:23 ;
A36: (hom f,a) . x = x * f by A10, A32, ENS_1:def 21;
then reconsider h = (hom f,a) . x as Morphism of A ;
A37: dom x = cod f by A32, CAT_1:18;
then A38: dom (x * f) = dom f by CAT_1:42;
dom (g * x) = dom x by A34, CAT_1:42
.= cod f by A32, CAT_1:18 ;
then A39: g * x in Hom (cod f),b by A35, CAT_1:18;
cod (x * f) = cod x by A37, CAT_1:42
.= dom g by A32, CAT_1:18 ;
then A40: (hom f,a) . x in Hom (dom f),(dom g) by A36, A38, CAT_1:18;
((hom f,b) * (hom (cod f),g)) . x = (hom f,b) . ((hom (cod f),g) . x) by A29, FUNCT_1:22
.= (hom f,b) . (g * x) by A32, ENS_1:def 20
.= (g * x) * f by A39, ENS_1:def 21
.= g * (x * f) by A33, CAT_1:43
.= g * h by A10, A32, ENS_1:def 21
.= (hom (dom f),g) . ((hom f,a) . x) by A40, ENS_1:def 20
.= ((hom (dom f),g) * (hom f,a)) . x by A23, A29, FUNCT_1:22 ;
hence ((hom f,b) * (hom (cod f),g)) . x = ((hom (dom f),g) * (hom f,a)) . x ; :: thesis: verum

end;

suppose A41: 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:21;
hence ((hom f,b) * (hom (cod f),g)) . x = ((hom (dom f),g) * (hom f,a)) . x by A41, FUNCT_2:def 1; :: thesis: verum

end;

end;

end;

A42: Hom (<|(dom f),?> . a),(<|(dom f),?> . b) <> {} by A8, CAT_1:126;
A43: cod g = b by A8, CAT_1:23;
reconsider f4 = t . a as Morphism of (EnsHom A) ;
A44: 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;
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 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;
A47: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)),(fId (Hom A)) #) by ENS_1:def 14;
then A48: cod f1 = (fCod (Hom A)) . f1
.= cod f19 by ENS_1:def 11
.= (f1 `1 ) `2 by ENS_1:def 5
.= [(Hom (cod f),b),(Hom (dom f),b)] `2 by A46, MCART_1:7
.= Hom (dom f),b by MCART_1:7 ;
A49: dom f4 = (fDom (Hom A)) . f4 by A47
.= dom f49 by ENS_1:def 10
.= (f4 `1 ) `1 by ENS_1:def 4
.= [(Hom (cod f),a),(Hom (dom f),a)] `1 by A44, MCART_1:7
.= Hom (cod f),a by MCART_1:7 ;
A50: cod f4 = (fCod (Hom A)) . f4 by A47
.= cod f49 by ENS_1:def 11
.= (f4 `1 ) `2 by ENS_1:def 5
.= [(Hom (cod f),a),(Hom (dom f),a)] `2 by A44, MCART_1:7
.= Hom (dom f),a by MCART_1:7 ;
reconsider f2 = <|(cod f),?> . g as Morphism of (EnsHom A) ;
A51: f2 = (hom?- (cod f)) . g by A8, NATTRA_1:def 1
.= [[(Hom (cod f),(dom g)),(Hom (cod f),(cod g))],(hom (cod f),g)] by ENS_1:def 22 ;
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 10
.= (f2 `1 ) `1 by ENS_1:def 4
.= [(Hom (cod f),(dom g)),(Hom (cod f),(cod g))] `1 by A51, MCART_1:7
.= Hom (cod f),(dom g) by MCART_1:7 ;
A53: cod f2 = (fCod (Hom A)) . f2 by A47
.= cod f29 by ENS_1:def 11
.= (f2 `1 ) `2 by ENS_1:def 5
.= [(Hom (cod f),(dom g)),(Hom (cod f),(cod g))] `2 by A51, MCART_1:7
.= Hom (cod f),(cod g) by MCART_1:7 ;
A54: dom f1 = (fDom (Hom A)) . f1 by A47
.= dom f19 by ENS_1:def 10
.= (f1 `1 ) `1 by ENS_1:def 4
.= [(Hom (cod f),b),(Hom (dom f),b)] `1 by A46, MCART_1:7
.= Hom (cod f),b by MCART_1:7 ;
then A55: cod f2 = dom f1 by A8, A53, CAT_1:23;
reconsider f3 = <|(dom f),?> . g as Morphism of (EnsHom A) ;
A56: f3 = (hom?- (dom f)) . g by A8, NATTRA_1:def 1
.= [[(Hom (dom f),(dom g)),(Hom (dom f),(cod g))],(hom (dom f),g)] by ENS_1:def 22 ;
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 11
.= (f3 `1 ) `2 by ENS_1:def 5
.= [(Hom (dom f),(dom g)),(Hom (dom f),(cod g))] `2 by A56, MCART_1:7
.= Hom (dom f),(cod g) by MCART_1:7 ;
A58: dom f3 = (fDom (Hom A)) . f3 by A47
.= dom f39 by ENS_1:def 10
.= (f3 `1 ) `1 by ENS_1:def 4
.= [(Hom (dom f),(dom g)),(Hom (dom f),(cod g))] `1 by A56, MCART_1:7
.= Hom (dom f),(dom g) by MCART_1:7 ;
then A59: cod f4 = dom f3 by A8, A50, CAT_1:23;
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 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 A10, A43, A23, A28, FUNCT_1:9
.= 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;

hence <|(cod f),?> is_naturally_transformable_to <|(dom f),?> by A7, NATTRA_1:def 7; :: thesis: verum