:: deftheorem Def6 defines export ISOCAT_2:def 6 :
for A, B, C being Category
for b₄ being Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) holds
( b₄ = export (A,B,C) iff 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 b₄ . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] );