f
in
Hom
(
a
,
b
)
by
A1
,
CAT_1:def 5
;
then
T
.
f
in
Hom
(
(
T
.
a
)
,
(
T
.
b
)
)
by
CAT_1:81
;
hence
T
.
f
is
Morphism
of
T
.
a
,
T
.
b
by
CAT_1:def 5
;
:: thesis:
verum