:: deftheorem defines ManySortedElement AOFA_A00:def 12 :
for I being set
for S, b₃ being ManySortedSet of I holds
( b₃ is ManySortedElement of S iff for i being set st i in I holds
b₃ . i is Element of S . i );