let IT1, IT2 be Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,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] = [[(export F1),(export F2)],(export 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] = [[(export F1),(export F2)],(export t)] ) implies IT1 = IT2 )
assume that
A23: 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] = [[(export F1),(export F2)],(export t)] and
A24: 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] = [[(export F1),(export F2)],(export 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, t being natural_transformation of F1,F2 such that
A25: F1 is_naturally_transformable_to F2 and
dom f = F1 and
cod f = F2 and
A26: f = [[F1,F2],t] by Th6;
thus IT1 . f = [[(export F1),(export F2)],(export t)] by A23, A25, A26
.= IT2 . f by A24, A25, A26 ; :: thesis: verum

end;

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