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)
A62: 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;
A63: cod m = (fCod (Hom A)) . m by A62
.= 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 A62
.= 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 A63, CAT_1:18; :: thesis: verum

end;

then for a being Object of A holds Hom (<|(cod f),?> . a),(<|(dom f),?> . a) <> {} ;
then A64: <|(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
A65: for o being Object of A holds h1 . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] and
A66: 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

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 A65
.= h2 . o by A66 ; :: thesis: verum

end;

hence h1 = h2 by A64, NATTRA_1:20; :: thesis: verum