:: deftheorem Def4 defines export ISOCAT_2:def 4 :
for A, B, C being Category
for F being Functor of [:A,B:],C
for b₅ being Functor of A, Functors (B,C) holds
( b₅ = export F iff for f being Morphism of A holds b₅ . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] );