let UA be Universal_Algebra; :: thesis: UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic
set G = UAEndMonoid UA;
set H = MSAEndMonoid (MSAlg UA);
ex h being Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) st h is bijective

proof

deffunc H₁( object ) -> set = 0 .--> $1;
consider h being Function such that
A1: ( dom h = UAEnd UA & ( for x being object st x in UAEnd UA holds
h . x = H₁(x) ) ) from FUNCT_1:sch 3();
reconsider h = h as Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) by A1, Th14;
h is bijective by A1, Th15;
hence ex h being Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) st h is bijective ; :: thesis: verum

end;

hence UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic ; :: thesis: verum