:: deftheorem defines 1-Alg MSUALG_1:def 14 :
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS holds 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #);