let UA be Universal_Algebra; :: thesis: UAAutGroup UA, MSAAutGroup (MSAlg UA) are_isomorphic

deffunc H_{1}( object ) -> set = 0 .--> $1;

consider h being Function such that

A1: ( dom h = UAAut UA & ( for x being object st x in UAAut UA holds

h . x = H_{1}(x) ) )
from FUNCT_1:sch 3();

reconsider h = h as Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) by A1, Th33;

take h ; :: according to GROUP_6:def 11 :: thesis: h is bijective

thus h is bijective by A1, Th34; :: thesis: verum

deffunc H

consider h being Function such that

A1: ( dom h = UAAut UA & ( for x being object st x in UAAut UA holds

h . x = H

reconsider h = h as Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) by A1, Th33;

take h ; :: according to GROUP_6:def 11 :: thesis: h is bijective

thus h is bijective by A1, Th34; :: thesis: verum