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
proof
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;
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 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