for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for f being Element of MSAAut U1 holds f in MSFuncs ( the Sorts of U1, the Sorts of U1) by Th20;