theorem :: CIRCCOMB:21

for S being non empty strict ManySortedSign
for A being non-empty MSAlgebra over S holds A +* A = MSAlgebra(# the Sorts of A, the Charact of A #)