:: deftheorem Def13 defines Projections_family CAT_3:def 13 :
for C being Category
for a being Object of C
for I being set
for b₄ being Function of I, the carrier' of C holds
( b₄ is Projections_family of a,I iff doms b₄ = I --> a );