:: deftheorem Def9 defines Carrier PRALG_2:def 9 :
for I being set
for S being non empty ManySortedSign
for s being SortSymbol of S
for A being MSAlgebra-Family of I,S
for b₅ being ManySortedSet of I holds
( ( I <> {} implies ( b₅ = Carrier (A,s) iff for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b₅ . i = the Sorts of U0 . s ) ) ) & ( not I <> {} implies ( b₅ = Carrier (A,s) iff b₅ = {} ) ) );