A3
: for
a
,
b
being
Object
of
A
st
Hom
(
a
,
b
)
<>
{}
holds
for
f
being
Morphism
of
a
,
b
holds
(
(
t1
"
)
.
b
)
*
(
F2
/.
f
)
=
(
F1
/.
f
)
*
(
(
t1
"
)
.
a
)
by
A1
,
A2
,
Lm4
;
F2
is_naturally_transformable_to
F1
by
A1
,
A2
,
Lm5
;
hence
t1
"
is
natural_transformation
of
F2
,
F1
by
A3
,
Def7
;
:: thesis:
verum