:: deftheorem defines is_a_product_wrt CAT_3:def 14 :
for C being Category
for a being Object of C
for I being set
for F being Function of I, the carrier' of C holds
( a is_a_product_wrt F iff ( F is Projections_family of a,I & ( for b being Object of C
for F9 being Projections_family of b,I st cods F = cods F9 holds
ex h being Morphism of C st
( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff h = k ) ) ) ) ) );