let UA be Universal_Algebra; :: thesis: UAAutGroup UA, MSAAutGroup (MSAlg UA) are_isomorphic
deffunc H1( 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 = H1(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