let IT1, IT2 be Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):]; :: thesis: ( ( for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT1 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) & ( for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT2 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) implies IT1 = IT2 )
assume that
A34: for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT1 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] and
A35: for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT2 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ; :: thesis: IT1 = IT2

now :: thesis: for f being Morphism of (Functors (A,[:B,C:])) holds IT1 . f = IT2 . f

let f be Morphism of (Functors (A,[:B,C:])); :: thesis: IT1 . f = IT2 . f
consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that
A36: F1 is_naturally_transformable_to F2 and
dom f = F1 and
cod f = F2 and
A37: f = [[F1,F2],s] by Th6;
thus IT1 . f = [[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] by A34, A36, A37
.= IT2 . f by A35, A36, A37 ; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:63; :: thesis: verum