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

set G = UAEndMonoid UA;

set H = MSAEndMonoid (MSAlg UA);

ex h being Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) st h is bijective

proof

hence
UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic
; :: thesis: verum
deffunc H_{1}( 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_{1}(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;consider h being Function such that

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

h . x = H

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