:: deftheorem Def7 defines ManySortedMSSet AOFA_A00:def 7 :
for I, J being set
for S1 being ManySortedSet of I
for S2 being ManySortedSet of J
for b₅ being ManySortedMSSet of S1,J holds
( b₅ is ManySortedMSSet of S1,S2 iff for i, a being set st i in I & a in S1 . i holds
(b₅ . i) . a is ManySortedSubset of S2 );