begin
definition
let UA be
Universal_Algebra;
func UAEnd UA -> FUNCTION_DOMAIN of the
carrier of
UA,the
carrier of
UA means :
Def1:
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 )
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
end;
:: deftheorem Def1 defines UAEnd ENDALG:def 1 :
theorem
theorem
canceled;
theorem Th3:
theorem Th4:
:: deftheorem Def2 defines UAEndComp ENDALG:def 2 :
:: deftheorem Def3 defines UAEndMonoid ENDALG:def 3 :
theorem Th5:
theorem
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:
( ( for
f being
Element of
it holds
f is
ManySortedFunction of ,
U1 ) & ( for
h being
ManySortedFunction of ,
U1 holds
(
h in it iff
h is_homomorphism U1,
U1 ) ) );
existence
ex b1 being MSFunctionSet of the Sorts of U1,the Sorts of U1 st
( ( for f being Element of b1 holds f is ManySortedFunction of ,U1 ) & ( for h being ManySortedFunction of ,U1 holds
( h in b1 iff h is_homomorphism U1,U1 ) ) )
uniqueness
for b1, b2 being MSFunctionSet of the Sorts of U1,the Sorts of U1 st ( for f being Element of b1 holds f is ManySortedFunction of ,U1 ) & ( for h being ManySortedFunction of ,U1 holds
( h in b1 iff h is_homomorphism U1,U1 ) ) & ( for f being Element of b2 holds f is ManySortedFunction of ,U1 ) & ( for h being ManySortedFunction of ,U1 holds
( h in b2 iff h is_homomorphism U1,U1 ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines MSAEnd ENDALG:def 4 :
theorem
canceled;
theorem
canceled;
theorem
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem Def5 defines MSAEndComp ENDALG:def 5 :
:: deftheorem Def6 defines MSAEndMonoid ENDALG:def 6 :
theorem Th13:
theorem
theorem
canceled;
theorem Th16:
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)
theorem Th17:
:: 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 :
theorem Th18:
theorem Th19:
theorem