:: deftheorem Def10 defines SORTS PRALG_2:def 10 :
for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S
for b₄ being ManySortedSet of the carrier of S holds
( b₄ = SORTS A iff for s being SortSymbol of S holds b₄ . s = product (Carrier (A,s)) );