:: deftheorem Def2 defines MSUnion CLOSURE3:def 2 :
for I being set
for M being ManySortedSet of I
for A being SubsetFamily of M
for b₄ being ManySortedSubset of M holds
( b₄ = MSUnion A iff for i being set st i in I holds
b₄ . i = union { (f . i) where f is Element of Bool M : f in A } );