:: deftheorem Def18 defines ConstOSA OSALG_1:def 18 :
for S being OrderSortedSign
for z being non empty set
for CH being ManySortedFunction of ((ConstOSSet (S,z)) #) * the Arity of S,(ConstOSSet (S,z)) * the ResultSort of S
for b₄ being strict non-empty MSAlgebra over S holds
( b₄ = ConstOSA (S,z,CH) iff ( the Sorts of b₄ = ConstOSSet (S,z) & the Charact of b₄ = CH ) );