:: deftheorem Def13 defines LeastSorts OSAFREE:def 13 :
for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for x being FinSequence of TS (DTConOSA X)
for b₄ being Element of the carrier of S * holds
( b₄ = LeastSorts x iff ( dom b₄ = dom x & ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & b₄ . y = LeastSort t ) ) ) );