theorem :: AUTALG_1:23

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds MSAAut U1 c= MSFuncs ( the Sorts of U1, the Sorts of U1) ;