:: deftheorem Def3 defines coprod MSAFREE:def 3 :
for I being set
for X being ManySortedSet of I
for b₃ being set holds
( b₃ = coprod X iff ( dom b₃ = I & ( for i being set st i in I holds
b₃ . i = coprod (i,X) ) ) );