:: deftheorem Def10 defines Coprod ALTCAT_6:def 10 :
for I being set
for E being non empty set
for A being ObjectsFamily of I,(EnsCat E)
for b₄ being ManySortedSet of I holds
( b₄ = Coprod A iff for i being object st i in I holds
ex F being Function of (A . i),(Union (coprod A)) st
( b₄ . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) ) );