let f1, f2 be Functor of Functors A,B,B; :: thesis: ( ( 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
A26:
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
A27:
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
; :: thesis: f1 = f2
now let c be
Morphism of
(Functors A,B);
:: thesis: 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 A28:
c = [[F1,F2],t]
and A29:
F1 is_naturally_transformable_to F2
by NATTRA_1:def 15;
thus f1 . c =
t . a
by A26, A28, A29
.=
f2 . c
by A27, A28, A29
;
:: thesis: verum end;
hence
f1 = f2
by FUNCT_2:113; :: thesis: verum