:: deftheorem defines projection-morphisms ALTCAT_5:def 6 :
for C being category
for I being set
for A being ObjectsFamily of I,C
for B being Object of C
for P being MorphismsFamily of B,A holds
( P is projection-morphisms iff for X being Object of C
for F being MorphismsFamily of X,A st F is feasible holds
ex f being Morphism of X,B st
( f in <^X,B^> & ( for i being set st i in I holds
ex si being Object of C ex Pi being Morphism of B,si st
( si = A . i & Pi = P . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,B st ( for i being set st i in I holds
ex si being Object of C ex Pi being Morphism of B,si st
( si = A . i & Pi = P . i & F . i = Pi * f1 ) ) holds
f = f1 ) ) );