:: deftheorem Def7 defines ManySortedFunctor INDEX_1:def 7 :
for A being non empty set
for F, G being ManySortedCategory of A
for b₄ being ManySortedFunction of A holds
( b₄ is ManySortedFunctor of F,G iff for a being Element of A holds b₄ . a is Functor of F . a,G . a );