:: deftheorem Def2 defines coprod MSAFREE:def 2 :
for I being set
for X being ManySortedSet of I
for i being object st i in I holds
for b₄ being set holds
( b₄ = coprod (i,X) iff for x being set holds
( x in b₄ iff ex a being set st
( a in X . i & x = [a,i] ) ) );