for UA being Universal_Algebra
for f, g being Function of UA,UA st f is Element of UAAut UA & g = f " holds
g is_isomorphism