theorem Th9: :: MSUALG_2:9

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds
MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)