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
A28: 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
A29: 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

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
A30: F1 is_naturally_transformable_to F2 and
A31: ( dom f = F1 & cod f = F2 & f = [[F1,F2],s] ) by Th9;
thus IT1 . f = [[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] by A28, A30, A31
.= IT2 . f by A29, A30, A31 ; :: thesis: verum

end;

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