(
F
is_naturally_transformable_to
F
& ( for
a
,
b
being
Object
of
A
st
<^
a
,
b
^>
<>
{}
holds
for
f
being
Morphism
of
a
,
b
holds
(
(
idt
F
)
!
b
)
*
(
F
.
f
)
=
(
F
.
f
)
*
(
(
idt
F
)
!
a
)
) )
by
Lm1
;
hence
idt
F
is
natural_transformation
of
F
,
F
by
Def7
;
:: thesis:
verum