let f1, f2 be Functor of Functors (A,B),B; ( ( for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
f1 . [[F1,F2],t] = t . a ) & ( for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
f2 . [[F1,F2],t] = t . a ) implies f1 = f2 )
assume that
A28:
for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
f1 . [[F1,F2],t] = t . a
and
A29:
for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
f2 . [[F1,F2],t] = t . a
; f1 = f2
now for c being Morphism of (Functors (A,B)) holds f1 . c = f2 . clet c be
Morphism of
(Functors (A,B));
f1 . c = f2 . c
the
carrier' of
(Functors (A,B)) = NatTrans (
A,
B)
by NATTRA_1:def 17;
then consider F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F1,
F2 such that A30:
(
c = [[F1,F2],t] &
F1 is_naturally_transformable_to F2 )
by NATTRA_1:def 15;
thus f1 . c =
t . a
by A28, A30
.=
f2 . c
by A29, A30
;
verum end;
hence
f1 = f2
by FUNCT_2:63; verum