theorem :: ENDALG:11

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 = 1_ (MSAEndMonoid U1) by Def6;