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
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 ; :: thesis: f1 = f2

now :: thesis: for c being Morphism of (Functors (A,B)) holds f1 . c = f2 . c

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 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 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum