set B = EnsHom A;
deffunc H₁( Element of A) -> object = [[(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
.= 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
.= 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 H₁(o) in the carrier' of (EnsHom A)

proof

let o be Object of A; :: thesis: H₁(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 H₁(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 = H₁(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;

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

suppose A15: 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;

suppose A16: 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 object ; :: 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;

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

suppose A20: 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;

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

let e be object ; :: 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

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

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 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 object 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 object ; :: 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: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;

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: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
.= 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
.= 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
.= 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
.= 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
.= 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
.= 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
.= 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
.= 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 b₁ being natural_transformation of <|(cod f),?>,<|(dom f),?> st
for o being Object of A holds b₁ . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ; :: thesis: verum