:: deftheorem Def16 defines Injections_family CAT_3:def 16 :
for C being Category
for c being Object of C
for I being set
for b₄ being Function of I, the carrier' of C holds
( b₄ is Injections_family of c,I iff cods b₄ = I --> c );