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

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
A26: ( dom f = F1 & cod f = F2 & f = [[F1,F2],t] ) by Th9;
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:113; :: thesis: verum