:: deftheorem Def6 defines ManySortedMSSet AOFA_A00:def 6 :
for I, J being set
for S being ManySortedSet of I
for b₄ being ManySortedFunction of I holds
( b₄ is ManySortedMSSet of S,J iff for i, j being set st i in I holds
( dom (b₄ . i) = S . i & ( j in S . i implies (b₄ . i) . j is ManySortedSet of J ) ) );