let UA be Universal_Algebra; :: thesis: for h being Homomorphism of (),(MSAEndMonoid (MSAlg UA)) st ( for x being object st x in UAEnd UA holds
h . x = 0 .--> x ) holds
h is bijective

reconsider e = id the Sorts of (MSAlg UA) as Element of MSAEnd (MSAlg UA) by Th7;
set N = multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),e #);
reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
let h be Homomorphism of (),(MSAEndMonoid (MSAlg UA)); :: thesis: ( ( for x being object st x in UAEnd UA holds
h . x = 0 .--> x ) implies h is bijective )

set G = UAEndMonoid UA;
set H = MSAEndMonoid (MSAlg UA);
set M = multLoopStr(# (UAEnd UA),(),i #);
1. multLoopStr(# (UAEnd UA),(),i #) = i ;
then A1: UAEndMonoid UA = multLoopStr(# (UAEnd UA),(),i #) by Def3;
assume A2: for x being object st x in UAEnd UA holds
h . x = 0 .--> x ; :: thesis: h is bijective
for a, b being Element of () st h . a = h . b holds
a = b
proof
let a, b be Element of (); :: thesis: ( h . a = h . b implies a = b )
assume A3: h . a = h . b ; :: thesis: a = b
A4: h . b = 0 .--> b by A2, A1
.= ;
h . a = 0 .--> a by A2, A1
.= ;
then {a} = {b} by ;
hence a = b by ZFMISC_1:3; :: thesis: verum
end;
then A5: h is one-to-one by GROUP_6:1;
1. multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),e #) = e ;
then A6: MSAEndMonoid (MSAlg UA) = multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),e #) by Def6;
dom h = UAEnd UA by ;
then rng h = the carrier of (MSAEndMonoid (MSAlg UA)) by A2, A6, Lm3;
then h is onto ;
hence h is bijective by A5; :: thesis: verum