:: deftheorem Def3 defines SingleAlg MSAFREE1:def 3 :
for S being non empty ManySortedSign
for b₂ being strict MSAlgebra over S holds
( b₂ = SingleAlg S iff for i being set st i in the carrier of S holds
the Sorts of b₂ . i = {i} );