begin
Lm1:
for UA being Universal_Algebra
for f being Function of UA,UA st f is_isomorphism UA,UA holds
f " is Function of UA,UA
Lm2:
for UA being Universal_Algebra
for f being Element of UAAut UA holds
( dom f = rng f & dom f = the carrier of UA )
begin
begin
Lm3:
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 is "1-1" & f is "onto" )
begin
Lm4:
for UA being Universal_Algebra
for h being Function st dom h = UAAut UA & ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) holds
rng h = MSAAut (MSAlg UA)