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
A30:
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
A31:
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 let c be
Morphism of
(Functors A,B);
f1 . c = f2 . c
the
carrier' of
(Functors A,B) = NatTrans A,
B
by NATTRA_1:def 18;
then consider F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F1,
F2 such that A32:
(
c = [[F1,F2],t] &
F1 is_naturally_transformable_to F2 )
by NATTRA_1:def 15;
thus f1 . c =
t . a
by A30, A32
.=
f2 . c
by A31, A32
;
verum end;
hence
f1 = f2
by FUNCT_2:113; verum