:: deftheorem Def1 defines { PZFMISC1:def 1 :
for I being set
for A, b₃ being ManySortedSet of I holds
( b₃ = {A} iff for i being object st i in I holds
b₃ . i = {(A . i)} );