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 b₁ being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st
for h being Function of UA,UA holds
( h in b₁ iff h is_homomorphism UA,UA )

proof end;

uniqueness
for b₁, b₂ being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st ( for h being Function of UA,UA holds
( h in b₁ iff h is_homomorphism UA,UA ) ) & ( for h being Function of UA,UA holds
( h in b₂ iff h is_homomorphism UA,UA ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines UAEnd ENDALG:def 1 :
for UA being Universal_Algebra
for b₂ being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA holds
( b₂ = UAEnd UA iff for h being Function of UA,UA holds
( h in b₂ 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 end;

theorem :: ENDALG:2

canceled;

theorem Th3: :: ENDALG:3

for UA being Universal_Algebra holds id the carrier of UA in UAEnd UA

proof end;

theorem Th4: :: ENDALG:4

for UA being Universal_Algebra
for f1, f2 being Element of UAEnd UA holds f1 * f2 in UAEnd UA

proof 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 b₁ being BinOp of (UAEnd UA) st
for x, y being Element of UAEnd UA holds b₁ . (x,y) = y * x

proof end;

uniqueness
for b₁, b₂ being BinOp of (UAEnd UA) st ( for x, y being Element of UAEnd UA holds b₁ . (x,y) = y * x ) & ( for x, y being Element of UAEnd UA holds b₂ . (x,y) = y * x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines UAEndComp ENDALG:def 2 :
for UA being Universal_Algebra
for b₂ being BinOp of (UAEnd UA) holds
( b₂ = UAEndComp UA iff for x, y being Element of UAEnd UA holds b₂ . (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 b₁ being strict multLoopStr st
( the carrier of b₁ = UAEnd UA & the multF of b₁ = UAEndComp UA & 1. b₁ = id the carrier of UA )

proof end;

uniqueness
for b₁, b₂ being strict multLoopStr st the carrier of b₁ = UAEnd UA & the multF of b₁ = UAEndComp UA & 1. b₁ = id the carrier of UA & the carrier of b₂ = UAEnd UA & the multF of b₂ = UAEndComp UA & 1. b₂ = id the carrier of UA holds
b₁ = b₂ ;

end;

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

registration

let UA be Universal_Algebra;
cluster UAEndMonoid UA -> non empty strict ;
coherence
not UAEndMonoid UA is empty

proof end;

end;

Lm1: now

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 )
set F = UAEndMonoid UA;
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:23 ; :: thesis: e * x = x
thus e * x = (UAEndComp UA) . (i,y) by Def3
.= y * i by Def2
.= x by A1, FUNCT_2:23 ; :: 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 end;

end;

theorem Th5: :: ENDALG:5

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

theorem :: ENDALG:6

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 of S;
func MSAEnd U1 -> MSFunctionSet of the Sorts of U1, the Sorts of 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 b₁ being MSFunctionSet of the Sorts of U1, the Sorts of U1 st
( ( for f being Element of b₁ holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b₁ iff h is_homomorphism U1,U1 ) ) )

proof end;

uniqueness
for b₁, b₂ being MSFunctionSet of the Sorts of U1, the Sorts of U1 st ( for f being Element of b₁ holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b₁ iff h is_homomorphism U1,U1 ) ) & ( for f being Element of b₂ holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b₂ iff h is_homomorphism U1,U1 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines MSAEnd ENDALG:def 4 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for b₃ being MSFunctionSet of the Sorts of U1, the Sorts of U1 holds
( b₃ = MSAEnd U1 iff ( ( for f being Element of b₃ holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b₃ iff h is_homomorphism U1,U1 ) ) ) );

theorem :: ENDALG:7

canceled;

theorem :: ENDALG:8

canceled;

theorem :: ENDALG:9

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S holds MSAEnd U1 c= product (MSFuncs ( the Sorts of U1, the Sorts of U1))

proof end;

theorem Th10: :: ENDALG:10

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S holds id the Sorts of U1 in MSAEnd U1

proof end;

theorem Th11: :: ENDALG:11

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for f1, f2 being Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1

proof end;

theorem Th12: :: ENDALG:12

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

definition

let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of 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 b₁ being BinOp of (MSAEnd U1) st
for x, y being Element of MSAEnd U1 holds b₁ . (x,y) = y ** x

proof end;

uniqueness
for b₁, b₂ being BinOp of (MSAEnd U1) st ( for x, y being Element of MSAEnd U1 holds b₁ . (x,y) = y ** x ) & ( for x, y being Element of MSAEnd U1 holds b₂ . (x,y) = y ** x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines MSAEndComp ENDALG:def 5 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for b₃ being BinOp of (MSAEnd U1) holds
( b₃ = MSAEndComp U1 iff for x, y being Element of MSAEnd U1 holds b₃ . (x,y) = y ** x );

definition

let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of 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 b₁ being strict multLoopStr st
( the carrier of b₁ = MSAEnd U1 & the multF of b₁ = MSAEndComp U1 & 1. b₁ = id the Sorts of U1 )

proof end;

uniqueness
for b₁, b₂ being strict multLoopStr st the carrier of b₁ = MSAEnd U1 & the multF of b₁ = MSAEndComp U1 & 1. b₁ = id the Sorts of U1 & the carrier of b₂ = MSAEnd U1 & the multF of b₂ = MSAEndComp U1 & 1. b₂ = id the Sorts of U1 holds
b₁ = b₂ ;

end;

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

registration

let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of S;
cluster MSAEndMonoid U1 -> non empty strict ;
coherence
not MSAEndMonoid U1 is empty

proof end;

end;

Lm2: now

let S be non empty non void ManySortedSign ; :: thesis: for U1 being non-empty MSAlgebra of 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 of 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 of S;
cluster MSAEndMonoid U1 -> strict associative well-unital ;
coherence
( MSAEndMonoid U1 is well-unital & MSAEndMonoid U1 is associative )

proof end;

end;

theorem Th13: :: ENDALG:13

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of 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 end;

theorem :: ENDALG:14

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

theorem :: ENDALG:15

canceled;

theorem Th16: :: ENDALG:16

for UA being Universal_Algebra
for f being Element of UAEnd UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)

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

registration

cluster non empty left_unital multLoopStr ;
existence
ex b₁ being non empty multLoopStr st b₁ is left_unital

proof 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 Element of bool [: the carrier of G, the carrier of H:];
existence
ex b₁ being Function of G,H st
( b₁ is multiplicative & b₁ is unity-preserving )

proof 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 Th17: :: ENDALG:17

for G being non empty well-unital multLoopStr holds id the carrier of G is Homomorphism of G,G

proof end;

definition

let G, H be non empty well-unital multLoopStr ;
canceled;
canceled;
canceled;
canceled;
canceled;
pred G,H are_isomorphic means :Def12: :: ENDALG:def 12
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 end;

end;

:: deftheorem ENDALG:def 7 :
canceled;

:: deftheorem ENDALG:def 8 :
canceled;

:: deftheorem ENDALG:def 9 :
canceled;

:: deftheorem ENDALG:def 10 :
canceled;

:: deftheorem ENDALG:def 11 :
canceled;

:: deftheorem Def12 defines are_isomorphic ENDALG:def 12 :
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 Th18: :: ENDALG:18

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

theorem Th19: :: ENDALG:19

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

theorem :: ENDALG:20

for UA being Universal_Algebra holds UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic

proof end;