let UA be Universal_Algebra; :: thesis: for h being Homomorphism of (UAEndMonoid UA),(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 (UAEndMonoid UA),(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),(UAEndComp UA),i #);

1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i ;

then A1: UAEndMonoid UA = multLoopStr(# (UAEnd UA),(UAEndComp 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 (UAEndMonoid UA) st h . a = h . b holds

a = b

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 A1, FUNCT_2:def 1;

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

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 (UAEndMonoid UA),(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),(UAEndComp UA),i #);

1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i ;

then A1: UAEndMonoid UA = multLoopStr(# (UAEnd UA),(UAEndComp 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 (UAEndMonoid UA) st h . a = h . b holds

a = b

proof

then A5:
h is one-to-one
by GROUP_6:1;
let a, b be Element of (UAEndMonoid UA); :: 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

.= [:{0},{b}:] ;

h . a = 0 .--> a by A2, A1

.= [:{0},{a}:] ;

then {a} = {b} by A3, A4, ZFMISC_1:110;

hence a = b by ZFMISC_1:3; :: thesis: verum

end;assume A3: h . a = h . b ; :: thesis: a = b

A4: h . b = 0 .--> b by A2, A1

.= [:{0},{b}:] ;

h . a = 0 .--> a by A2, A1

.= [:{0},{a}:] ;

then {a} = {b} by A3, A4, ZFMISC_1:110;

hence a = b by ZFMISC_1:3; :: thesis: verum

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 A1, FUNCT_2:def 1;

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