let UA be Universal_Algebra; :: thesis: for h being Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) st ( for x being set st x in UAEnd UA holds
h . x = 0 .--> x ) holds
h is bijective
let h be Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)); :: thesis: ( ( for x being set st x in UAEnd UA holds
h . x = 0 .--> x ) implies h is bijective )
assume A1: for x being set st x in UAEnd UA holds
h . x = 0 .--> x ; :: thesis: h is bijective
set G = UAEndMonoid UA;
reconsider i = id the carrier of UA as Element of UAEnd UA by Th3;
set H = MSAEndMonoid (MSAlg UA);
set M = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #);
1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i ;
then A2: UAEndMonoid UA = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) by Def3;
reconsider e = id the Sorts of (MSAlg UA) as Element of MSAEnd (MSAlg UA) by Th10;
set N = multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),e #);
1. multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),e #) = e ;
then A3: MSAEndMonoid (MSAlg UA) = multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),e #) by Def6;
thus h is bijective :: thesis: verum

proof

thus h is one-to-one :: according to FUNCT_2:def 4 :: thesis: h is onto

proof

thus h is one-to-one :: thesis: verum

proof

for a, b being Element of (UAEndMonoid UA) st h . a = h . b holds
a = b

proof

let a, b be Element of (UAEndMonoid UA); :: thesis: ( h . a = h . b implies a = b )
assume A4: h . a = h . b ; :: thesis: a = b
A5: h . a = 0 .--> a by A1, A2
.= [:{0 },{a}:] ;
h . b = 0 .--> b by A1, A2
.= [:{0 },{b}:] ;
then {a} = {b} by A4, A5, ZFMISC_1:134;
hence a = b by ZFMISC_1:6; :: thesis: verum

end;

hence h is one-to-one by GROUP_6:1; :: thesis: verum

end;

end;

thus h is onto :: thesis: verum

proof

dom h = UAEnd UA by A2, FUNCT_2:def 1;
hence rng h = the carrier of (MSAEndMonoid (MSAlg UA)) by A1, A3, Lm3; :: according to FUNCT_2:def 3 :: thesis: verum

end;

end;