theorem Th7: :: ENDALG:7

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSAEnd U1