let S be non empty non void ManySortedSign ; :: thesis: for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSAAut U1
let U1 be non-empty MSAlgebra over S; :: thesis: id the Sorts of U1 in MSAAut U1
id the Sorts of U1 is_isomorphism U1,U1 by MSUALG_3:16;
hence id the Sorts of U1 in MSAAut U1 by Def5; :: thesis: verum