:: deftheorem Def9 defines TargetCat INDEX_1:def 9 :
for A, B being non empty set
for F, G being Function of B,A
for I being Indexing of F,G
for b₆ being Categorial Category holds
( b₆ is TargetCat of I iff ( ( for a being Element of A holds (I `1) . a is Object of b<sub>6</sub> ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of b₆ ) ) );