:: deftheorem Def5 defines export ISOCAT_2:def 5 :
for A, B, C being Category
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
for b₇ being natural_transformation of export F1, export F2 holds
( b₇ = export t iff for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds b₇ . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] );