:: deftheorem Def5 defines MSAAut AUTALG_1:def 5 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for b₃ being MSFunctionSet of U1,U1 holds
( b₃ = MSAAut U1 iff for h being ManySortedFunction of U1,U1 holds
( h in b₃ iff h is_isomorphism U1,U1 ) );