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

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

proof

then
for a being Object of A holds Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) <> {}
;
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

.= 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

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

.= 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

.= 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

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

hence
h1 = h2
by A62, NATTRA_1:19; :: thesis: verumlet 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;thus h1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] by A63

.= h2 . o by A64 ; :: thesis: verum