:: ENDALG semantic presentation

begin

definition
let UA be Universal_Algebra;
func UAEnd UA ->  FUNCTION_DOMAIN of the carrier of UA, the carrier of UA means :Def1: :: ENDALG:def 1
 for h being Function of UA,UA holds
( h in it iff h is_homomorphism UA,UA );
existence
 ex b1 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st
for h being Function of UA,UA holds
( h in b1 iff h is_homomorphism UA,UA )
proof
set F =  {  x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA  }  ;
A1: id the carrier of UA in  {  x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA  }
proof
set I = id the carrier of UA;
 ( id the carrier of UA in Funcs ( the carrier of UA, the carrier of UA) & id the carrier of UA is_homomorphism UA,UA ) by ALG_1:5, FUNCT_2:8;
hence  id the carrier of UA in  {  x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA  }  ; ::_thesis: verum
end;
  {  x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA  }  is functional
proof
let q be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not q in  {  x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA  }  or q is set )
assume  q in  {  x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA  }  ; ::_thesis: q is set
then  ex x being Element of Funcs ( the carrier of UA, the carrier of UA) st
( q = x & x is_homomorphism UA,UA ) ;
hence  q is set ; ::_thesis: verum
end;
then reconsider F =  {  x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA  }  as functional non empty set by A1;
 F is FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
proof
let a be Element of F; :: according to FUNCT_2:def_12 ::_thesis: a is Element of bool [: the carrier of UA, the carrier of UA:]
 a in F ;
then  ex x being Element of Funcs ( the carrier of UA, the carrier of UA) st
( a = x & x is_homomorphism UA,UA ) ;
hence  a is Element of bool [: the carrier of UA, the carrier of UA:] ; ::_thesis: verum
end;
then reconsider F = F as FUNCTION_DOMAIN of the carrier of UA, the carrier of UA ;
take  F ; ::_thesis: for h being Function of UA,UA holds
( h in F iff h is_homomorphism UA,UA )
let h be Function of UA,UA; ::_thesis: ( h in F iff h is_homomorphism UA,UA )
thus  ( h in F implies h is_homomorphism UA,UA ) ::_thesis: ( h is_homomorphism UA,UA implies h in F )
proof
assume  h in F ; ::_thesis: h is_homomorphism UA,UA
then  ex f being Element of Funcs ( the carrier of UA, the carrier of UA) st
( f = h & f is_homomorphism UA,UA ) ;
hence  h is_homomorphism UA,UA ; ::_thesis: verum
end;
A2: h is Element of Funcs ( the carrier of UA, the carrier of UA) by FUNCT_2:8;
assume  h is_homomorphism UA,UA ; ::_thesis: h in F
hence  h in F by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st ( for h being Function of UA,UA holds
( h in b1 iff h is_homomorphism UA,UA ) ) & ( for h being Function of UA,UA holds
( h in b2 iff h is_homomorphism UA,UA ) ) holds
b1 = b2
proof
let F1, F2 be FUNCTION_DOMAIN of the carrier of UA, the carrier of UA; ::_thesis: ( ( for h being Function of UA,UA holds
( h in F1 iff h is_homomorphism UA,UA ) ) & ( for h being Function of UA,UA holds
( h in F2 iff h is_homomorphism UA,UA ) ) implies F1 = F2 )
assume that
A3: for h being Function of UA,UA holds
( h in F1 iff h is_homomorphism UA,UA ) and
A4: for h being Function of UA,UA holds
( h in F2 iff h is_homomorphism UA,UA ) ; ::_thesis: F1 = F2
A5: for f being Element of F2 holds f is Function of UA,UA ;
A6: F2 c= F1
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F2 or q in F1 )
assume A7: q in F2 ; ::_thesis: q in F1
then reconsider h1 = q as Function of UA,UA by A5;
 h1 is_homomorphism UA,UA by A4, A7;
hence  q in F1 by A3; ::_thesis: verum
end;
A8: for f being Element of F1 holds f is Function of UA,UA ;
 F1 c= F2
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F1 or q in F2 )
assume A9: q in F1 ; ::_thesis: q in F2
then reconsider h1 = q as Function of UA,UA by A8;
 h1 is_homomorphism UA,UA by A3, A9;
hence  q in F2 by A4; ::_thesis: verum
end;
hence  F1 = F2 by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines UAEnd ENDALG:def_1_:_
 for UA being Universal_Algebra
for b2 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA holds
( b2 = UAEnd UA iff for h being Function of UA,UA holds
( h in b2 iff h is_homomorphism UA,UA ) );

theorem :: ENDALG:1
for UA being Universal_Algebra holds UAEnd UA c= Funcs ( the carrier of UA, the carrier of UA)
proof
let UA be Universal_Algebra; ::_thesis: UAEnd UA c= Funcs ( the carrier of UA, the carrier of UA)
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in UAEnd UA or q in Funcs ( the carrier of UA, the carrier of UA) )
assume  q in UAEnd UA ; ::_thesis: q in Funcs ( the carrier of UA, the carrier of UA)
then  q is Element of UAEnd UA ;
hence  q in Funcs ( the carrier of UA, the carrier of UA) by FUNCT_2:9; ::_thesis: verum
end;

theorem Th2: :: ENDALG:2
for UA being Universal_Algebra holds id the carrier of UA in UAEnd UA
proof
let UA be Universal_Algebra; ::_thesis: id the carrier of UA in UAEnd UA
 id the carrier of UA is_homomorphism UA,UA by ALG_1:5;
hence  id the carrier of UA in UAEnd UA by Def1; ::_thesis: verum
end;

theorem Th3: :: ENDALG:3
for UA being Universal_Algebra
for f1, f2 being Element of UAEnd UA holds f1 * f2 in UAEnd UA
proof
let UA be Universal_Algebra; ::_thesis: for f1, f2 being Element of UAEnd UA holds f1 * f2 in UAEnd UA
let f1, f2 be Element of UAEnd UA; ::_thesis: f1 * f2 in UAEnd UA
 ( f1 is_homomorphism UA,UA & f2 is_homomorphism UA,UA ) by Def1;
then  f1 * f2 is_homomorphism UA,UA by ALG_1:6;
hence  f1 * f2 in UAEnd UA by Def1; ::_thesis: verum
end;

definition
let UA be Universal_Algebra;
func UAEndComp UA ->  BinOp of (UAEnd UA) means :Def2: :: ENDALG:def 2
 for x, y being Element of UAEnd UA holds it . (x,y) = y * x;
existence
 ex b1 being BinOp of (UAEnd UA) st
for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x
proof
defpred S1[ Element of UAEnd UA, Element of UAEnd UA, set ] means $3 = $2 * $1;
A1: for x, y being Element of UAEnd UA ex m being Element of UAEnd UA st S1[x,y,m]
proof
let x, y be Element of UAEnd UA; ::_thesis: ex m being Element of UAEnd UA st S1[x,y,m]
reconsider xx = x, yy = y as Function of UA,UA ;
reconsider m = yy * xx as Element of UAEnd UA by Th3;
take  m ; ::_thesis: S1[x,y,m]
thus  S1[x,y,m] ; ::_thesis: verum
end;
 ex B being BinOp of (UAEnd UA) st
for x, y being Element of UAEnd UA holds S1[x,y,B . (x,y)] from BINOP_1:sch_3(A1);
hence  ex b1 being BinOp of (UAEnd UA) st
for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (UAEnd UA) st ( for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x ) & ( for x, y being Element of UAEnd UA holds b2 . (x,y) = y * x ) holds
b1 = b2
proof
let b1, b2 be BinOp of (UAEnd UA); ::_thesis: ( ( for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x ) & ( for x, y being Element of UAEnd UA holds b2 . (x,y) = y * x ) implies b1 = b2 )
assume that
A2: for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x and
A3: for x, y being Element of UAEnd UA holds b2 . (x,y) = y * x ; ::_thesis: b1 = b2
 for x, y being Element of UAEnd UA holds b1 . (x,y) = b2 . (x,y)
proof
let x, y be Element of UAEnd UA; ::_thesis: b1 . (x,y) = b2 . (x,y)
thus b1 . (x,y) = y * x by A2
.= b2 . (x,y) by A3 ; ::_thesis: verum
end;
hence  b1 = b2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines UAEndComp ENDALG:def_2_:_
 for UA being Universal_Algebra
for b2 being BinOp of (UAEnd UA) holds
( b2 = UAEndComp UA iff for x, y being Element of UAEnd UA holds b2 . (x,y) = y * x );

definition
let UA be Universal_Algebra;
func UAEndMonoid UA ->  strict multLoopStr  means :Def3: :: ENDALG:def 3
( the carrier of it = UAEnd UA & the multF of it = UAEndComp UA & 1. it = id the carrier of UA );
existence
 ex b1 being strict multLoopStr st
( the carrier of b1 = UAEnd UA & the multF of b1 = UAEndComp UA & 1. b1 = id the carrier of UA )
proof
reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
take  multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) ; ::_thesis: ( the carrier of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = UAEnd UA & the multF of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = UAEndComp UA & 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = id the carrier of UA )
thus  ( the carrier of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = UAEnd UA & the multF of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = UAEndComp UA & 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = id the carrier of UA ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict multLoopStr st the carrier of b1 = UAEnd UA & the multF of b1 = UAEndComp UA & 1. b1 = id the carrier of UA & the carrier of b2 = UAEnd UA & the multF of b2 = UAEndComp UA & 1. b2 = id the carrier of UA holds
b1 = b2 ;
end;

:: deftheorem Def3 defines UAEndMonoid ENDALG:def_3_:_
 for UA being Universal_Algebra
for b2 being strict multLoopStr holds
( b2 = UAEndMonoid UA iff ( the carrier of b2 = UAEnd UA & the multF of b2 = UAEndComp UA & 1. b2 = id the carrier of UA ) );

registration
let UA be Universal_Algebra;
cluster UAEndMonoid UA ->  non empty strict ;
coherence
 not UAEndMonoid UA is empty
proof
reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
set M = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #);
 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i ;
hence  not UAEndMonoid UA is empty by Def3; ::_thesis: verum
end;
end;

Lm1: now__::_thesis:_for_UA_being_Universal_Algebra
for_x,_e_being_Element_of_(UAEndMonoid_UA)_st_e_=_id_the_carrier_of_UA_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let UA be Universal_Algebra; ::_thesis: for x, e being Element of (UAEndMonoid UA) st e = id the carrier of UA holds
( x * e = x & e * x = x )
let x, e be Element of (UAEndMonoid UA); ::_thesis: ( e = id the carrier of UA implies ( x * e = x & e * x = x ) )
reconsider i = e, y = x as Element of UAEnd UA by Def3;
assume A1: e = id the carrier of UA ; ::_thesis: ( x * e = x & e * x = x )
thus x * e = (UAEndComp UA) . (y,i) by Def3
.= i * y by Def2
.= x by A1, FUNCT_2:17 ; ::_thesis: e * x = x
thus e * x = (UAEndComp UA) . (i,y) by Def3
.= y * i by Def2
.= x by A1, FUNCT_2:17 ; ::_thesis: verum
end;

registration
let UA be Universal_Algebra;
cluster UAEndMonoid UA ->  strict associative well-unital ;
coherence
 ( UAEndMonoid UA is well-unital & UAEndMonoid UA is associative )
proof
reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
set H = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #);
thus  UAEndMonoid UA is well-unital ::_thesis: UAEndMonoid UA is associative
proof
let x be Element of (UAEndMonoid UA); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (UAEndMonoid UA)) = x & (1. (UAEndMonoid UA)) * x = x )
 1. (UAEndMonoid UA) = i by Def3;
hence  ( x * (1. (UAEndMonoid UA)) = x & (1. (UAEndMonoid UA)) * x = x ) by Lm1; ::_thesis: verum
end;
 for f, g, h being Element of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) holds (f * g) * h = f * (g * h)
proof
let f, g, h be Element of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #); ::_thesis: (f * g) * h = f * (g * h)
reconsider A = f, B = g, C = h as Element of UAEnd UA ;
A1: g * h = C * B by Def2;
 f * g = B * A by Def2;
hence (f * g) * h = C * (B * A) by Def2
.= (C * B) * A by RELAT_1:36
.= f * (g * h) by A1, Def2 ;
::_thesis: verum
end;
then  ( 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i & multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) is associative ) by GROUP_1:def_3;
hence  UAEndMonoid UA is associative by Def3; ::_thesis: verum
end;
end;

theorem Th4: :: ENDALG:4
for UA being Universal_Algebra
for x, y being Element of (UAEndMonoid UA)
for f, g being Element of UAEnd UA st x = f & y = g holds
x * y = g * f
proof
let UA be Universal_Algebra; ::_thesis: for x, y being Element of (UAEndMonoid UA)
for f, g being Element of UAEnd UA st x = f & y = g holds
x * y = g * f
reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
let x, y be Element of (UAEndMonoid UA); ::_thesis: for f, g being Element of UAEnd UA st x = f & y = g holds
x * y = g * f
let f, g be Element of UAEnd UA; ::_thesis: ( x = f & y = g implies x * y = g * f )
set H = 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  ( x = f & y = g ) ; ::_thesis: x * y = g * f
hence  x * y = g * f by A1, Def2; ::_thesis: verum
end;

theorem :: ENDALG:5
for UA being Universal_Algebra holds id the carrier of UA = 1_ (UAEndMonoid UA) by Def3;


definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
set T = the Sorts of U1;
func MSAEnd U1 ->  MSFunctionSet of U1,U1 means :Def4: :: ENDALG:def 4
( ( for f being Element of it holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in it iff h is_homomorphism U1,U1 ) ) );
existence
 ex b1 being MSFunctionSet of U1,U1 st
( ( for f being Element of b1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b1 iff h is_homomorphism U1,U1 ) ) )
proof
defpred S1[ set ] means  ex msf being ManySortedFunction of U1,U1 st
( $1 = msf & msf is_homomorphism U1,U1 );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in MSFuncs ( the Sorts of U1, the Sorts of U1) & S1[x] ) ) from XBOOLE_0:sch_1();
 ( id the Sorts of U1 in MSFuncs ( the Sorts of U1, the Sorts of U1) & ex F being ManySortedFunction of U1,U1 st
( id the Sorts of U1 = F & F is_homomorphism U1,U1 ) ) by AUTALG_1:20, MSUALG_3:9;
then reconsider X = X as non empty set by A1;
 X c= MSFuncs ( the Sorts of U1, the Sorts of U1)
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X or q in MSFuncs ( the Sorts of U1, the Sorts of U1) )
thus  ( not q in X or q in MSFuncs ( the Sorts of U1, the Sorts of U1) ) by A1; ::_thesis: verum
end;
then reconsider X = X as MSFunctionSet of U1,U1 ;
take  X ; ::_thesis: ( ( for f being Element of X holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in X iff h is_homomorphism U1,U1 ) ) )
thus  for f being Element of X holds f is ManySortedFunction of U1,U1 ; ::_thesis: for h being ManySortedFunction of U1,U1 holds
( h in X iff h is_homomorphism U1,U1 )
let h be ManySortedFunction of U1,U1; ::_thesis: ( h in X iff h is_homomorphism U1,U1 )
hereby  ::_thesis: ( h is_homomorphism U1,U1 implies h in X )
assume  h in X ; ::_thesis: h is_homomorphism U1,U1
then  ex msf being ManySortedFunction of U1,U1 st
( h = msf & msf is_homomorphism U1,U1 ) by A1;
hence  h is_homomorphism U1,U1 ; ::_thesis: verum
end;
 h in MSFuncs ( the Sorts of U1, the Sorts of U1) by AUTALG_1:20;
hence  ( h is_homomorphism U1,U1 implies h in X ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being MSFunctionSet of U1,U1 st ( for f being Element of b1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b1 iff h is_homomorphism U1,U1 ) ) & ( for f being Element of b2 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b2 iff h is_homomorphism U1,U1 ) ) holds
b1 = b2
proof
let F1, F2 be MSFunctionSet of U1,U1; ::_thesis: ( ( for f being Element of F1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in F1 iff h is_homomorphism U1,U1 ) ) & ( for f being Element of F2 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in F2 iff h is_homomorphism U1,U1 ) ) implies F1 = F2 )
assume that
A3: for f being Element of F1 holds f is ManySortedFunction of U1,U1 and
A4: for h being ManySortedFunction of U1,U1 holds
( h in F1 iff h is_homomorphism U1,U1 ) and
A5: for f being Element of F2 holds f is ManySortedFunction of U1,U1 and
A6: for h being ManySortedFunction of U1,U1 holds
( h in F2 iff h is_homomorphism U1,U1 ) ; ::_thesis: F1 = F2
A7: F2 c= F1
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F2 or q in F1 )
assume A8: q in F2 ; ::_thesis: q in F1
then reconsider h1 = q as ManySortedFunction of U1,U1 by A5;
 h1 is_homomorphism U1,U1 by A6, A8;
hence  q in F1 by A4; ::_thesis: verum
end;
 F1 c= F2
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F1 or q in F2 )
assume A9: q in F1 ; ::_thesis: q in F2
then reconsider h1 = q as ManySortedFunction of U1,U1 by A3;
 h1 is_homomorphism U1,U1 by A4, A9;
hence  q in F2 by A6; ::_thesis: verum
end;
hence  F1 = F2 by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines MSAEnd ENDALG:def_4_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for b3 being MSFunctionSet of U1,U1 holds
( b3 = MSAEnd U1 iff ( ( for f being Element of b3 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b3 iff h is_homomorphism U1,U1 ) ) ) );

theorem :: ENDALG:6
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds MSAEnd U1 c= MSFuncs ( the Sorts of U1, the Sorts of U1) ;

theorem Th7: :: ENDALG:7
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSAEnd U1
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSAEnd U1
let U1 be non-empty MSAlgebra over S; ::_thesis: id the Sorts of U1 in MSAEnd U1
 id the Sorts of U1 is_homomorphism U1,U1 by MSUALG_3:9;
hence  id the Sorts of U1 in MSAEnd U1 by Def4; ::_thesis: verum
end;

theorem Th8: :: ENDALG:8
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for f1, f2 being Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S
for f1, f2 being Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1
let U1 be non-empty MSAlgebra over S; ::_thesis: for f1, f2 being Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1
let f1, f2 be Element of MSAEnd U1; ::_thesis: f1 ** f2 in MSAEnd U1
 ( f1 is_homomorphism U1,U1 & f2 is_homomorphism U1,U1 ) by Def4;
then  f1 ** f2 is_homomorphism U1,U1 by MSUALG_3:10;
hence  f1 ** f2 in MSAEnd U1 by Def4; ::_thesis: verum
end;

theorem Th9: :: ENDALG:9
for UA being Universal_Algebra
for F being ManySortedFunction of (MSAlg UA),(MSAlg UA)
for f being Element of UAEnd UA st F = 0 .--> f holds
F in MSAEnd (MSAlg UA)
proof
let UA be Universal_Algebra; ::_thesis: for F being ManySortedFunction of (MSAlg UA),(MSAlg UA)
for f being Element of UAEnd UA st F = 0 .--> f holds
F in MSAEnd (MSAlg UA)
let F be ManySortedFunction of (MSAlg UA),(MSAlg UA); ::_thesis: for f being Element of UAEnd UA st F = 0 .--> f holds
F in MSAEnd (MSAlg UA)
let f be Element of UAEnd UA; ::_thesis: ( F = 0 .--> f implies F in MSAEnd (MSAlg UA) )
assume  F = 0 .--> f ; ::_thesis: F in MSAEnd (MSAlg UA)
then A1: F = MSAlg f by MSUHOM_1:def_3;
 f is_homomorphism UA,UA by Def1;
then  MSAlg f is_homomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:16;
then  F is_homomorphism MSAlg UA, MSAlg UA by A1, MSUHOM_1:9;
hence  F in MSAEnd (MSAlg UA) by Def4; ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
func MSAEndComp U1 ->  BinOp of (MSAEnd U1) means :Def5: :: ENDALG:def 5
 for x, y being Element of MSAEnd U1 holds it . (x,y) = y ** x;
existence
 ex b1 being BinOp of (MSAEnd U1) st
for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x
proof
defpred S1[ Element of MSAEnd U1, Element of MSAEnd U1, set ] means $3 = $2 ** $1;
A1: for x, y being Element of MSAEnd U1 ex m being Element of MSAEnd U1 st S1[x,y,m]
proof
let x, y be Element of MSAEnd U1; ::_thesis: ex m being Element of MSAEnd U1 st S1[x,y,m]
reconsider xx = x, yy = y as ManySortedFunction of U1,U1 ;
reconsider m = yy ** xx as Element of MSAEnd U1 by Th8;
take  m ; ::_thesis: S1[x,y,m]
thus  S1[x,y,m] ; ::_thesis: verum
end;
 ex B being BinOp of (MSAEnd U1) st
for x, y being Element of MSAEnd U1 holds S1[x,y,B . (x,y)] from BINOP_1:sch_3(A1);
hence  ex b1 being BinOp of (MSAEnd U1) st
for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (MSAEnd U1) st ( for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x ) & ( for x, y being Element of MSAEnd U1 holds b2 . (x,y) = y ** x ) holds
b1 = b2
proof
let b1, b2 be BinOp of (MSAEnd U1); ::_thesis: ( ( for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x ) & ( for x, y being Element of MSAEnd U1 holds b2 . (x,y) = y ** x ) implies b1 = b2 )
assume that
A2: for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x and
A3: for x, y being Element of MSAEnd U1 holds b2 . (x,y) = y ** x ; ::_thesis: b1 = b2
 for x, y being Element of MSAEnd U1 holds b1 . (x,y) = b2 . (x,y)
proof
let x, y be Element of MSAEnd U1; ::_thesis: b1 . (x,y) = b2 . (x,y)
thus b1 . (x,y) = y ** x by A2
.= b2 . (x,y) by A3 ; ::_thesis: verum
end;
hence  b1 = b2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines MSAEndComp ENDALG:def_5_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for b3 being BinOp of (MSAEnd U1) holds
( b3 = MSAEndComp U1 iff for x, y being Element of MSAEnd U1 holds b3 . (x,y) = y ** x );

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
func MSAEndMonoid U1 ->  strict multLoopStr  means :Def6: :: ENDALG:def 6
( the carrier of it = MSAEnd U1 & the multF of it = MSAEndComp U1 & 1. it = id the Sorts of U1 );
existence
 ex b1 being strict multLoopStr st
( the carrier of b1 = MSAEnd U1 & the multF of b1 = MSAEndComp U1 & 1. b1 = id the Sorts of U1 )
proof
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
take H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #); ::_thesis: ( the carrier of H = MSAEnd U1 & the multF of H = MSAEndComp U1 & 1. H = id the Sorts of U1 )
thus  the carrier of H = MSAEnd U1 ; ::_thesis: ( the multF of H = MSAEndComp U1 & 1. H = id the Sorts of U1 )
thus  the multF of H = MSAEndComp U1 ; ::_thesis: 1. H = id the Sorts of U1
thus  1. H = id the Sorts of U1 ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict multLoopStr st the carrier of b1 = MSAEnd U1 & the multF of b1 = MSAEndComp U1 & 1. b1 = id the Sorts of U1 & the carrier of b2 = MSAEnd U1 & the multF of b2 = MSAEndComp U1 & 1. b2 = id the Sorts of U1 holds
b1 = b2 ;
end;

:: deftheorem Def6 defines MSAEndMonoid ENDALG:def_6_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for b3 being strict multLoopStr holds
( b3 = MSAEndMonoid U1 iff ( the carrier of b3 = MSAEnd U1 & the multF of b3 = MSAEndComp U1 & 1. b3 = id the Sorts of U1 ) );

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
cluster MSAEndMonoid U1 ->  non empty strict ;
coherence
 not MSAEndMonoid U1 is empty
proof
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
set H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #);
 1. multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) = i ;
hence  not MSAEndMonoid U1 is empty by Def6; ::_thesis: verum
end;
end;

Lm2: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_
for_U1_being_non-empty_MSAlgebra_over_S
for_x,_e_being_Element_of_(MSAEndMonoid_U1)_st_e_=_id_the_Sorts_of_U1_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S
for x, e being Element of (MSAEndMonoid U1) st e = id the Sorts of U1 holds
( x * e = x & e * x = x )
let U1 be non-empty MSAlgebra over S; ::_thesis: for x, e being Element of (MSAEndMonoid U1) st e = id the Sorts of U1 holds
( x * e = x & e * x = x )
set F = MSAEndMonoid U1;
let x, e be Element of (MSAEndMonoid U1); ::_thesis: ( e = id the Sorts of U1 implies ( x * e = x & e * x = x ) )
reconsider i = e, y = x as Element of MSAEnd U1 by Def6;
assume A1: e = id the Sorts of U1 ; ::_thesis: ( x * e = x & e * x = x )
thus x * e = (MSAEndComp U1) . (y,i) by Def6
.= i ** y by Def5
.= x by A1, MSUALG_3:4 ; ::_thesis: e * x = x
thus e * x = (MSAEndComp U1) . (i,y) by Def6
.= y ** i by Def5
.= x by A1, MSUALG_3:3 ; ::_thesis: verum
end;

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
cluster MSAEndMonoid U1 ->  strict associative well-unital ;
coherence
 ( MSAEndMonoid U1 is well-unital & MSAEndMonoid U1 is associative )
proof
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
set H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #);
thus  MSAEndMonoid U1 is well-unital ::_thesis: MSAEndMonoid U1 is associative
proof
let x be Element of (MSAEndMonoid U1); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (MSAEndMonoid U1)) = x & (1. (MSAEndMonoid U1)) * x = x )
 1. (MSAEndMonoid U1) = i by Def6;
hence  ( x * (1. (MSAEndMonoid U1)) = x & (1. (MSAEndMonoid U1)) * x = x ) by Lm2; ::_thesis: verum
end;
 for f, g, h being Element of multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) holds (f * g) * h = f * (g * h)
proof
let f, g, h be Element of multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #); ::_thesis: (f * g) * h = f * (g * h)
reconsider A = f, B = g, C = h as Element of MSAEnd U1 ;
A1: g * h = C ** B by Def5;
 f * g = B ** A by Def5;
hence (f * g) * h = C ** (B ** A) by Def5
.= (C ** B) ** A by PBOOLE:140
.= f * (g * h) by A1, Def5 ;
::_thesis: verum
end;
then  ( 1. multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) = i & multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) is associative ) by GROUP_1:def_3;
hence  MSAEndMonoid U1 is associative by Def6; ::_thesis: verum
end;
end;

theorem Th10: :: ENDALG:10
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for x, y being Element of (MSAEndMonoid U1)
for f, g being Element of MSAEnd U1 st x = f & y = g holds
x * y = g ** f
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S
for x, y being Element of (MSAEndMonoid U1)
for f, g being Element of MSAEnd U1 st x = f & y = g holds
x * y = g ** f
let U1 be non-empty MSAlgebra over S; ::_thesis: for x, y being Element of (MSAEndMonoid U1)
for f, g being Element of MSAEnd U1 st x = f & y = g holds
x * y = g ** f
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
let x, y be Element of (MSAEndMonoid U1); ::_thesis: for f, g being Element of MSAEnd U1 st x = f & y = g holds
x * y = g ** f
let f, g be Element of MSAEnd U1; ::_thesis: ( x = f & y = g implies x * y = g ** f )
set H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #);
 1. multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) = i ;
then A1: MSAEndMonoid U1 = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) by Def6;
assume  ( x = f & y = g ) ; ::_thesis: x * y = g ** f
hence  x * y = g ** f by A1, Def5; ::_thesis: verum
end;

theorem :: ENDALG:11
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 = 1_ (MSAEndMonoid U1) by Def6;

theorem Th12: :: ENDALG:12
for UA being Universal_Algebra
for f being Element of UAEnd UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)
proof
let UA be Universal_Algebra; ::_thesis: for f being Element of UAEnd UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)
let f be Element of UAEnd UA; ::_thesis: 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)
 MSAlg f is ManySortedFunction of (MSAlg UA),(MSAlg UA) by MSUHOM_1:9;
hence  0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA) by MSUHOM_1:def_3; ::_thesis: verum
end;

Lm3:  for UA being Universal_Algebra
for h being Function st dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds
h . x = 0 .--> x ) holds
rng h = MSAEnd (MSAlg UA)
proof
let UA be Universal_Algebra; ::_thesis: for h being Function st dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds
h . x = 0 .--> x ) holds
rng h = MSAEnd (MSAlg UA)
let h be Function; ::_thesis: ( dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds
h . x = 0 .--> x ) implies rng h = MSAEnd (MSAlg UA) )
assume that
A1: dom h = UAEnd UA and
A2: for x being set st x in UAEnd UA holds
h . x = 0 .--> x ; ::_thesis: rng h = MSAEnd (MSAlg UA)
A3: MSAEnd (MSAlg UA) c= rng h
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MSAEnd (MSAlg UA) or x in rng h )
assume A4: x in MSAEnd (MSAlg UA) ; ::_thesis: x in rng h
then reconsider f = x as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Def4;
 the carrier of (MSSign UA) = {0} by MSUALG_1:def_8;
then A5: f = 0 .--> (f . 0) by AUTALG_1:11;
A6: f is_homomorphism MSAlg UA, MSAlg UA by A4, Def4;
 ex q being set st
( q in dom h & x = h . q )
proof
take q = f . 0; ::_thesis: ( q in dom h & x = h . q )
 f is ManySortedFunction of (MSAlg UA),((MSAlg UA) Over (MSSign UA)) by MSUHOM_1:9;
then reconsider q9 = q as Function of UA,UA by AUTALG_1:31;
 MSAlg q9 = f by A5, MSUHOM_1:def_3;
then  MSAlg q9 is_homomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by A6, MSUHOM_1:9;
then  q9 is_homomorphism UA,UA by MSUHOM_1:21;
hence  q in dom h by A1, Def1; ::_thesis: x = h . q
hence  x = h . q by A1, A2, A5; ::_thesis: verum
end;
hence  x in rng h by FUNCT_1:def_3; ::_thesis: verum
end;
 rng h c= MSAEnd (MSAlg UA)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng h or x in MSAEnd (MSAlg UA) )
assume  x in rng h ; ::_thesis: x in MSAEnd (MSAlg UA)
then consider q being set  such that
A7: q in dom h and
A8: x = h . q by FUNCT_1:def_3;
consider q9 being Element of UAEnd UA such that
A9: q9 = q by A1, A7;
 ( x = 0 .--> q & 0 .--> q is ManySortedFunction of (MSAlg UA),(MSAlg UA) ) by A1, A2, A7, A8, Th12;
then consider d being ManySortedFunction of (MSAlg UA),(MSAlg UA) such that
A10: d = x ;
 q9 is_homomorphism UA,UA by Def1;
then A11: MSAlg q9 is_homomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:16;
MSAlg q9 = 0 .--> q by A9, MSUHOM_1:def_3
.= x by A1, A2, A7, A8 ;
then  d is_homomorphism MSAlg UA, MSAlg UA by A10, A11, MSUHOM_1:9;
hence  x in MSAEnd (MSAlg UA) by A10, Def4; ::_thesis: verum
end;
hence  rng h = MSAEnd (MSAlg UA) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

registration
cluster non empty left_unital for multLoopStr ;
existence
 ex b1 being non empty multLoopStr st b1 is left_unital
proof
set m = the BinOp of {0};
set u = the Element of {0};
take  multLoopStr(# {0}, the BinOp of {0}, the Element of {0} #) ; ::_thesis: multLoopStr(# {0}, the BinOp of {0}, the Element of {0} #) is left_unital
let x be Element of multLoopStr(# {0}, the BinOp of {0}, the Element of {0} #); :: according to VECTSP_1:def_8 ::_thesis: (1. multLoopStr(# {0}, the BinOp of {0}, the Element of {0} #)) * x = x
thus (1. multLoopStr(# {0}, the BinOp of {0}, the Element of {0} #)) * x = 0 by TARSKI:def_1
.= x by TARSKI:def_1 ; ::_thesis: verum
end;
end;

registration
let G, H be non empty well-unital multLoopStr ;
cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving multiplicative for Element of bool [: the carrier of G, the carrier of H:];
existence
 ex b1 being Function of G,H st
( b1 is multiplicative & b1 is unity-preserving )
proof
reconsider m = the carrier of G --> (1. H) as Function of the carrier of G, the carrier of H ;
reconsider m = m as Function of G,H ;
take  m ; ::_thesis: ( m is multiplicative & m is unity-preserving )
 for x, y being Element of G holds m . (x * y) = (m . x) * (m . y)
proof
let x, y be Element of G; ::_thesis: m . (x * y) = (m . x) * (m . y)
m . (x * y) = 1. H by FUNCOP_1:7
.= (1. H) * (1. H) by VECTSP_1:def_8
.= (m . x) * (1. H) by FUNCOP_1:7
.= (m . x) * (m . y) by FUNCOP_1:7 ;
hence  m . (x * y) = (m . x) * (m . y) ; ::_thesis: verum
end;
hence  m is multiplicative by GROUP_6:def_6; ::_thesis: m is unity-preserving
thus  m . (1_ G) = 1_ H by FUNCOP_1:7; :: according to GROUP_1:def_13 ::_thesis: verum
end;
end;

definition
let G, H be non empty well-unital multLoopStr ;
mode Homomorphism of G,H is unity-preserving multiplicative Function of G,H;
end;

theorem Th13: :: ENDALG:13
for G being non empty well-unital multLoopStr holds id the carrier of G is Homomorphism of G,G
proof
let G be non empty well-unital multLoopStr ; ::_thesis: id the carrier of G is Homomorphism of G,G
reconsider f = id the carrier of G as Function of G,G ;
A1: for a, b being Element of G holds f . (a * b) = (f . a) * (f . b)
proof
let a, b be Element of G; ::_thesis: f . (a * b) = (f . a) * (f . b)
f . (a * b) = a * b by FUNCT_1:18
.= (f . a) * b by FUNCT_1:18
.= (f . a) * (f . b) by FUNCT_1:18 ;
hence  f . (a * b) = (f . a) * (f . b) ; ::_thesis: verum
end;
 f . (1_ G) = 1_ G by FUNCT_1:18;
hence  id the carrier of G is Homomorphism of G,G by A1, GROUP_1:def_13, GROUP_6:def_6; ::_thesis: verum
end;

definition
let G, H be non empty well-unital multLoopStr ;
predG,H are_isomorphic  means :Def7: :: ENDALG:def 7
 ex h being Homomorphism of G,H st h is bijective ;
reflexivity
 for G being non empty well-unital multLoopStr ex h being Homomorphism of G,G st h is bijective
proof
let G be non empty well-unital multLoopStr ; ::_thesis: ex h being Homomorphism of G,G st h is bijective
reconsider i = id the carrier of G as Homomorphism of G,G by Th13;
A1: the carrier of G c= rng i
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of G or y in rng i )
assume A2: y in the carrier of G ; ::_thesis: y in rng i
 ex x being set st
( x in dom i & y = i . x )
proof
take  y ; ::_thesis: ( y in dom i & y = i . y )
thus  ( y in dom i & y = i . y ) by A2, FUNCT_1:17; ::_thesis: verum
end;
hence  y in rng i by FUNCT_1:def_3; ::_thesis: verum
end;
 rng i c= the carrier of G by RELAT_1:def_19;
then  rng i = the carrier of G by A1, XBOOLE_0:def_10;
then  i is onto by FUNCT_2:def_3;
hence  ex h being Homomorphism of G,G st h is bijective ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines are_isomorphic ENDALG:def_7_:_
 for G, H being non empty well-unital multLoopStr holds
( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective );

theorem Th14: :: ENDALG:14
for UA being Universal_Algebra
for h being Function st dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds
h . x = 0 .--> x ) holds
h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA))
proof
let UA be Universal_Algebra; ::_thesis: for h being Function st dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds
h . x = 0 .--> x ) holds
h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA))
reconsider i = id the Sorts of (MSAlg UA) as Element of MSAEnd (MSAlg UA) by Th7;
set G = UAEndMonoid UA;
set H = MSAEndMonoid (MSAlg UA);
set M = multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),i #);
reconsider e = id the carrier of UA as Element of UAEnd UA by Th2;
let h be Function; ::_thesis: ( dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds
h . x = 0 .--> x ) implies h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) )
assume that
A1: dom h = UAEnd UA and
A2: for x being set st x in UAEnd UA holds
h . x = 0 .--> x ; ::_thesis: h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA))
A3: the carrier of (UAEndMonoid UA) = dom h by A1, Def3;
 1. multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),i #) = i ;
then A4: MSAEndMonoid (MSAlg UA) = multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),i #) by Def6;
then  rng h c= the carrier of (MSAEndMonoid (MSAlg UA)) by A1, A2, Lm3;
then reconsider h9 = h as Function of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) by A3, FUNCT_2:def_1, RELSET_1:4;
A5: h9 . e = 0 .--> e by A2;
A6: for a, b being Element of (UAEndMonoid UA) holds h9 . (a * b) = (h9 . a) * (h9 . b)
proof
let a, b be Element of (UAEndMonoid UA); ::_thesis: h9 . (a * b) = (h9 . a) * (h9 . b)
reconsider a9 = a, b9 = b as Element of UAEnd UA by Def3;
reconsider A = 0 .--> a9, B = 0 .--> b9 as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Th12;
reconsider ha = h9 . a, hb = h9 . b as Element of MSAEnd (MSAlg UA) by Def6;
A7: h9 . (b9 * a9) = 0 .--> (b9 * a9) by A2, Th3;
reconsider A9 = A, B9 = B as Element of (MSAEndMonoid (MSAlg UA)) by A4, Th9;
A8: ( ha = A9 & hb = B9 ) by A2;
thus h9 . (a * b) = h9 . (b9 * a9) by Th4
.= MSAlg (b9 * a9) by A7, MSUHOM_1:def_3
.= (MSAlg b9) ** (MSAlg a9) by MSUHOM_1:26
.= B ** (MSAlg a9) by MSUHOM_1:def_3
.= B ** A by MSUHOM_1:def_3
.= (h9 . a) * (h9 . b) by A8, Th10 ; ::_thesis: verum
end;
h9 . (1. (UAEndMonoid UA)) = h9 . e by Def3
.= MSAlg e by A5, MSUHOM_1:def_3
.= i by MSUHOM_1:25
.= 1_ (MSAEndMonoid (MSAlg UA)) by Def6 ;
then  h9 . (1_ (UAEndMonoid UA)) = 1_ (MSAEndMonoid (MSAlg UA)) ;
hence  h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) by A6, GROUP_1:def_13, GROUP_6:def_6; ::_thesis: verum
end;

theorem Th15: :: ENDALG:15
for UA being Universal_Algebra
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
proof
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
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 set 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 set 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 by FUNCT_2:def_3;
hence  h is bijective by A5; ::_thesis: verum
end;

theorem :: ENDALG:16
for UA being Universal_Algebra holds UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic
proof
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
proof
deffunc H1( set ) ->  set = 0 .--> $1;
consider h being Function such that
A1: ( dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds
h . x = H1(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;
hence  UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic by Def7; ::_thesis: verum
end;