:: deftheorem Def1 defines Flatten MSAFREE1:def 1 :
for I being non empty set
for X being disjoint_valued ManySortedSet of I
for D being non-empty ManySortedSet of I
for F being ManySortedFunction of X,D
for b₅ being Function of (Union X),(Union D) holds
( b₅ = Flatten F iff for i being Element of I
for x being set st x in X . i holds
b₅ . x = (F . i) . x );