theorem Th17: :: EQUATION:17

for S being non empty non void ManySortedSign
for A being MSAlgebra over S holds A is MSSubAlgebra of MSAlgebra(# the Sorts of A, the Charact of A #) by MSUALG_2:5;