:: deftheorem Def1 defines Carrier PCS_0:def 1 :
for I being non empty set
for C being 1-sorted-yielding ManySortedSet of I
for b₃ being ManySortedSet of I holds
( b₃ = Carrier C iff for i being Element of I holds b₃ . i = the carrier of (C . i) );