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

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