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;
[[(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;
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),?>; ( ( 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)))]
; h1 = h2
hence
h1 = h2
by A62, NATTRA_1:19; verum