begin
theorem Th1:
definition
let UA be
Universal_Algebra;
func UAAut 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_isomorphism 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_isomorphism 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_isomorphism UA,UA ) ) & ( for h being Function of UA,UA holds
( h in b2 iff h is_isomorphism UA,UA ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines UAAut AUTALG_1:def 1 :
theorem
theorem
canceled;
theorem Th4:
theorem
Lm1:
for UA being Universal_Algebra
for f being Function of UA,UA st f is_isomorphism UA,UA holds
f " is Function of UA,UA
theorem Th6:
theorem Th7:
:: deftheorem Def2 defines UAAutComp AUTALG_1:def 2 :
:: deftheorem defines UAAutGroup AUTALG_1:def 3 :
Lm2:
for UA being Universal_Algebra
for f being Element of UAAut UA holds
( dom f = rng f & dom f = the carrier of UA )
theorem
theorem Th9:
theorem
begin
theorem
theorem Th12:
theorem
canceled;
theorem Th14:
theorem
theorem Th16:
theorem Th17:
theorem
theorem Th19:
begin
theorem
canceled;
theorem Th21:
theorem Th22:
theorem Th23:
:: deftheorem AUTALG_1:def 4 :
canceled;
:: deftheorem AUTALG_1:def 5 :
canceled;
:: deftheorem Def6 defines MSFunctionSet AUTALG_1:def 6 :
theorem
theorem
theorem
canceled;
theorem
definition
let S be non
empty non
void ManySortedSign ;
let U1 be
non-empty MSAlgebra of
S;
func MSAAut U1 -> MSFunctionSet of the
Sorts of
U1,the
Sorts of
U1 means :
Def7:
for
h being
ManySortedFunction of ,
U1 holds
(
h in it iff
h is_isomorphism U1,
U1 );
existence
ex b1 being MSFunctionSet of the Sorts of U1,the Sorts of U1 st
for h being ManySortedFunction of ,U1 holds
( h in b1 iff h is_isomorphism U1,U1 )
uniqueness
for b1, b2 being MSFunctionSet of the Sorts of U1,the Sorts of U1 st ( for h being ManySortedFunction of ,U1 holds
( h in b1 iff h is_isomorphism U1,U1 ) ) & ( for h being ManySortedFunction of ,U1 holds
( h in b2 iff h is_isomorphism U1,U1 ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines MSAAut AUTALG_1:def 7 :
theorem
canceled;
theorem
theorem
Lm3:
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for f being Element of MSAAut U1 holds
( f is "1-1" & f is "onto" )
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
:: deftheorem Def8 defines MSAAutComp AUTALG_1:def 8 :
:: deftheorem defines MSAAutGroup AUTALG_1:def 9 :
theorem
theorem Th36:
theorem
begin
theorem Th38:
theorem Th39:
Lm4:
for UA being Universal_Algebra
for h being Function st dom h = UAAut UA & ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) holds
rng h = MSAAut (MSAlg UA)
theorem Th40:
theorem Th41:
theorem