:: AUTALG_1 semantic presentation

begin


theorem Th1: :: AUTALG_1:1
for UA being Universal_Algebra holds id the carrier of UA is_isomorphism UA,UA
proof
let UA be Universal_Algebra; ::_thesis: id the carrier of UA is_isomorphism UA,UA
set I = id the carrier of UA;
 id the carrier of UA is_homomorphism UA,UA by ALG_1:5;
hence  id the carrier of UA is_monomorphism UA,UA by ALG_1:def_2; :: according to ALG_1:def_4 ::_thesis: id the carrier of UA is_epimorphism UA,UA
 ( id the carrier of UA is_homomorphism UA,UA & rng (id the carrier of UA) = the carrier of UA ) by ALG_1:5, RELAT_1:45;
hence  id the carrier of UA is_epimorphism UA,UA by ALG_1:def_3; ::_thesis: verum
end;

definition
let UA be Universal_Algebra;
func UAAut UA ->  FUNCTION_DOMAIN of the carrier of UA, the carrier of UA means :Def1: :: AUTALG_1:def 1
 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 )
proof
set F =  {  x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_isomorphism 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_isomorphism 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_isomorphism UA,UA ) by Th1, 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_isomorphism UA,UA  }  ; ::_thesis: verum
end;
reconsider F =  {  x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_isomorphism UA,UA  }  as set ;
 F is functional
proof
let q be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not q in F or q is set )
assume  q in F ; ::_thesis: q is set
then  ex x being Element of Funcs ( the carrier of UA, the carrier of UA) st
( q = x & x is_isomorphism UA,UA ) ;
hence  q is set ; ::_thesis: verum
end;
then reconsider F = F 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_isomorphism 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_isomorphism UA,UA )
let h be Function of UA,UA; ::_thesis: ( h in F iff h is_isomorphism UA,UA )
thus  ( h in F implies h is_isomorphism UA,UA ) ::_thesis: ( h is_isomorphism UA,UA implies h in F )
proof
assume  h in F ; ::_thesis: h is_isomorphism UA,UA
then  ex f being Element of Funcs ( the carrier of UA, the carrier of UA) st
( f = h & f is_isomorphism UA,UA ) ;
hence  h is_isomorphism 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_isomorphism 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_isomorphism UA,UA ) ) & ( for h being Function of UA,UA holds
( h in b2 iff h is_isomorphism 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_isomorphism UA,UA ) ) & ( for h being Function of UA,UA holds
( h in F2 iff h is_isomorphism UA,UA ) ) implies F1 = F2 )
assume that
A3: for h being Function of UA,UA holds
( h in F1 iff h is_isomorphism UA,UA ) and
A4: for h being Function of UA,UA holds
( h in F2 iff h is_isomorphism UA,UA ) ; ::_thesis: F1 = F2
A5: F2 c= F1
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F2 or q in F1 )
assume A6: q in F2 ; ::_thesis: q in F1
then reconsider h1 = q as Function of UA,UA by FUNCT_2:def_12;
 h1 is_isomorphism UA,UA by A4, A6;
hence  q in F1 by A3; ::_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 A7: q in F1 ; ::_thesis: q in F2
then reconsider h1 = q as Function of UA,UA by FUNCT_2:def_12;
 h1 is_isomorphism UA,UA by A3, A7;
hence  q in F2 by A4; ::_thesis: verum
end;
hence  F1 = F2 by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

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

theorem :: AUTALG_1:2
for UA being Universal_Algebra holds UAAut UA c= Funcs ( the carrier of UA, the carrier of UA)
proof
let UA be Universal_Algebra; ::_thesis: UAAut UA c= Funcs ( the carrier of UA, the carrier of UA)
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in UAAut UA or q in Funcs ( the carrier of UA, the carrier of UA) )
assume  q in UAAut UA ; ::_thesis: q in Funcs ( the carrier of UA, the carrier of UA)
then  ex f being Element of UAAut UA st f = q ;
hence  q in Funcs ( the carrier of UA, the carrier of UA) by FUNCT_2:9; ::_thesis: verum
end;

theorem Th3: :: AUTALG_1:3
for UA being Universal_Algebra holds id the carrier of UA in UAAut UA
proof
let UA be Universal_Algebra; ::_thesis: id the carrier of UA in UAAut UA
 id the carrier of UA is_isomorphism UA,UA by Th1;
hence  id the carrier of UA in UAAut UA by Def1; ::_thesis: verum
end;

theorem :: AUTALG_1:4
for UA being Universal_Algebra
for f, g being Function of UA,UA st f is Element of UAAut UA & g = f " holds
g is_isomorphism UA,UA
proof
let UA be Universal_Algebra; ::_thesis: for f, g being Function of UA,UA st f is Element of UAAut UA & g = f " holds
g is_isomorphism UA,UA
let f, g be Function of UA,UA; ::_thesis: ( f is Element of UAAut UA & g = f " implies g is_isomorphism UA,UA )
assume that
A1: f is Element of UAAut UA and
A2: g = f " ; ::_thesis: g is_isomorphism UA,UA
 f is_isomorphism UA,UA by A1, Def1;
hence  g is_isomorphism UA,UA by A2, ALG_1:10; ::_thesis: verum
end;

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
proof
let UA be Universal_Algebra; ::_thesis: for f being Function of UA,UA st f is_isomorphism UA,UA holds
f " is Function of UA,UA
let f be Function of UA,UA; ::_thesis: ( f is_isomorphism UA,UA implies f " is Function of UA,UA )
assume A1: f is_isomorphism UA,UA ; ::_thesis: f " is Function of UA,UA
then  f is_epimorphism UA,UA by ALG_1:def_4;
then A2: rng f = the carrier of UA by ALG_1:def_3;
 f is one-to-one by A1, ALG_1:7;
hence  f " is Function of UA,UA by A2, FUNCT_2:25; ::_thesis: verum
end;

theorem Th5: :: AUTALG_1:5
for UA being Universal_Algebra
for f being Element of UAAut UA holds f " in UAAut UA
proof
let UA be Universal_Algebra; ::_thesis: for f being Element of UAAut UA holds f " in UAAut UA
let f be Element of UAAut UA; ::_thesis: f " in UAAut UA
A1: f is_isomorphism UA,UA by Def1;
then  f " is Function of UA,UA by Lm1;
then consider ff being Function of UA,UA such that
A2: ff = f " ;
 ff is_isomorphism UA,UA by A1, A2, ALG_1:10;
hence  f " in UAAut UA by A2, Def1; ::_thesis: verum
end;

theorem Th6: :: AUTALG_1:6
for UA being Universal_Algebra
for f1, f2 being Element of UAAut UA holds f1 * f2 in UAAut UA
proof
let UA be Universal_Algebra; ::_thesis: for f1, f2 being Element of UAAut UA holds f1 * f2 in UAAut UA
let f1, f2 be Element of UAAut UA; ::_thesis: f1 * f2 in UAAut UA
 ( f1 is_isomorphism UA,UA & f2 is_isomorphism UA,UA ) by Def1;
then  f1 * f2 is_isomorphism UA,UA by ALG_1:11;
hence  f1 * f2 in UAAut UA by Def1; ::_thesis: verum
end;

definition
let UA be Universal_Algebra;
func UAAutComp UA ->  BinOp of (UAAut UA) means :Def2: :: AUTALG_1:def 2
 for x, y being Element of UAAut UA holds it . (x,y) = y * x;
existence
 ex b1 being BinOp of (UAAut UA) st
for x, y being Element of UAAut UA holds b1 . (x,y) = y * x
proof
defpred S1[ Element of UAAut UA, Element of UAAut UA, set ] means $3 = $2 * $1;
A1: for x, y being Element of UAAut UA ex m being Element of UAAut UA st S1[x,y,m]
proof
let x, y be Element of UAAut UA; ::_thesis: ex m being Element of UAAut UA st S1[x,y,m]
reconsider xx = x, yy = y as Function of UA,UA ;
reconsider m = yy * xx as Element of UAAut UA by Th6;
take  m ; ::_thesis: S1[x,y,m]
thus  S1[x,y,m] ; ::_thesis: verum
end;
thus  ex IT being BinOp of (UAAut UA) st
for x, y being Element of UAAut UA holds S1[x,y,IT . (x,y)] from BINOP_1:sch_3(A1); ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (UAAut UA) st ( for x, y being Element of UAAut UA holds b1 . (x,y) = y * x ) & ( for x, y being Element of UAAut UA holds b2 . (x,y) = y * x ) holds
b1 = b2
proof
let b1, b2 be BinOp of (UAAut UA); ::_thesis: ( ( for x, y being Element of UAAut UA holds b1 . (x,y) = y * x ) & ( for x, y being Element of UAAut UA holds b2 . (x,y) = y * x ) implies b1 = b2 )
assume that
A2: for x, y being Element of UAAut UA holds b1 . (x,y) = y * x and
A3: for x, y being Element of UAAut UA holds b2 . (x,y) = y * x ; ::_thesis: b1 = b2
 for x, y being Element of UAAut UA holds b1 . (x,y) = b2 . (x,y)
proof
let x, y be Element of UAAut 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 UAAutComp AUTALG_1:def_2_:_
 for UA being Universal_Algebra
for b2 being BinOp of (UAAut UA) holds
( b2 = UAAutComp UA iff for x, y being Element of UAAut UA holds b2 . (x,y) = y * x );

definition
let UA be Universal_Algebra;
func UAAutGroup UA ->  Group equals :: AUTALG_1:def 3
 multMagma(# (UAAut UA),(UAAutComp UA) #);
coherence
 multMagma(# (UAAut UA),(UAAutComp UA) #) is Group
proof
set H = multMagma(# (UAAut UA),(UAAutComp UA) #);
A1: ex e being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st
for h being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st
( h * g = e & g * h = e ) )
proof
reconsider e = id the carrier of UA as Element of multMagma(# (UAAut UA),(UAAutComp UA) #) by Th3;
take  e ; ::_thesis: for h being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st
( h * g = e & g * h = e ) )
let h be Element of multMagma(# (UAAut UA),(UAAutComp UA) #); ::_thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st
( h * g = e & g * h = e ) )
consider A being Element of UAAut UA such that
A2: A = h ;
h * e = (id the carrier of UA) * A by A2, Def2
.= A by FUNCT_2:17 ;
hence  h * e = h by A2; ::_thesis: ( e * h = h & ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st
( h * g = e & g * h = e ) )
e * h = A * (id the carrier of UA) by A2, Def2
.= A by FUNCT_2:17 ;
hence  e * h = h by A2; ::_thesis: ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st
( h * g = e & g * h = e )
reconsider g = A " as Element of multMagma(# (UAAut UA),(UAAutComp UA) #) by Th5;
take  g ; ::_thesis: ( h * g = e & g * h = e )
A3: A is_isomorphism UA,UA by Def1;
then A4: A is one-to-one by ALG_1:7;
 A is_epimorphism UA,UA by A3, ALG_1:def_4;
then A5: rng A = the carrier of UA by ALG_1:def_3;
thus h * g = (A ") * A by A2, Def2
.= e by A4, A5, FUNCT_2:29 ; ::_thesis: g * h = e
thus g * h = A * (A ") by A2, Def2
.= e by A4, A5, FUNCT_2:29 ; ::_thesis: verum
end;
 for f, g, h being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) holds (f * g) * h = f * (g * h)
proof
let f, g, h be Element of multMagma(# (UAAut UA),(UAAutComp UA) #); ::_thesis: (f * g) * h = f * (g * h)
reconsider A = f, B = g, C = h as Element of UAAut UA ;
A6: 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 A6, Def2 ;
::_thesis: verum
end;
hence  multMagma(# (UAAut UA),(UAAutComp UA) #) is Group by A1, GROUP_1:def_2, GROUP_1:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines UAAutGroup AUTALG_1:def_3_:_
 for UA being Universal_Algebra holds UAAutGroup UA = multMagma(# (UAAut UA),(UAAutComp UA) #);

registration
let UA be Universal_Algebra;
cluster UAAutGroup UA ->  strict ;
coherence
 UAAutGroup UA is strict ;
end;

Lm2:  for UA being Universal_Algebra
for f being Element of UAAut UA holds
( dom f = rng f & dom f = the carrier of UA )
proof
let UA be Universal_Algebra; ::_thesis: for f being Element of UAAut UA holds
( dom f = rng f & dom f = the carrier of UA )
let f be Element of UAAut UA; ::_thesis: ( dom f = rng f & dom f = the carrier of UA )
A1: f is_isomorphism UA,UA by Def1;
then  dom f = the carrier of UA by ALG_1:8;
hence  ( dom f = rng f & dom f = the carrier of UA ) by A1, ALG_1:8; ::_thesis: verum
end;

theorem :: AUTALG_1:7
for UA being Universal_Algebra
for x, y being Element of (UAAutGroup UA)
for f, g being Element of UAAut UA st x = f & y = g holds
x * y = g * f by Def2;

theorem Th8: :: AUTALG_1:8
for UA being Universal_Algebra holds id the carrier of UA = 1_ (UAAutGroup UA)
proof
let UA be Universal_Algebra; ::_thesis: id the carrier of UA = 1_ (UAAutGroup UA)
set f = the Element of (UAAutGroup UA);
reconsider g = id the carrier of UA as Element of (UAAutGroup UA) by Th3;
consider g1 being Function of the carrier of UA, the carrier of UA such that
A1: g1 = g ;
 the Element of (UAAutGroup UA) is Element of UAAut UA ;
then consider f1 being Function of the carrier of UA, the carrier of UA such that
A2: f1 = the Element of (UAAutGroup UA) ;
g * the Element of (UAAutGroup UA) = f1 * g1 by A1, A2, Def2
.= the Element of (UAAutGroup UA) by A1, A2, FUNCT_2:17 ;
hence  id the carrier of UA = 1_ (UAAutGroup UA) by GROUP_1:7; ::_thesis: verum
end;

theorem :: AUTALG_1:9
for UA being Universal_Algebra
for f being Element of UAAut UA
for g being Element of (UAAutGroup UA) st f = g holds
f " = g "
proof
let UA be Universal_Algebra; ::_thesis: for f being Element of UAAut UA
for g being Element of (UAAutGroup UA) st f = g holds
f " = g "
let f be Element of UAAut UA; ::_thesis: for g being Element of (UAAutGroup UA) st f = g holds
f " = g "
let g be Element of (UAAutGroup UA); ::_thesis: ( f = g implies f " = g " )
consider g1 being Element of UAAut UA such that
A1: g1 = g " ;
assume  f = g ; ::_thesis: f " = g "
then  g1 * f = g * (g ") by A1, Def2;
then  g1 * f = 1_ (UAAutGroup UA) by GROUP_1:def_5;
then A2: g1 * f = id the carrier of UA by Th8;
 f is_isomorphism UA,UA by Def1;
then  f is_monomorphism UA,UA by ALG_1:def_4;
then A3: f is one-to-one by ALG_1:def_2;
rng f = dom f by Lm2
.= the carrier of UA by Lm2 ;
hence  f " = g " by A1, A3, A2, FUNCT_2:30; ::_thesis: verum
end;

begin


theorem :: AUTALG_1:10
for I being set
for A, B, C being ManySortedSet of I st A is_transformable_to B & B is_transformable_to C holds
A is_transformable_to C
proof
let I be set ; ::_thesis: for A, B, C being ManySortedSet of I st A is_transformable_to B & B is_transformable_to C holds
A is_transformable_to C
let A, B, C be ManySortedSet of I; ::_thesis: ( A is_transformable_to B & B is_transformable_to C implies A is_transformable_to C )
assume that
A1: A is_transformable_to B and
A2: B is_transformable_to C ; ::_thesis: A is_transformable_to C
let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in I or not C . i = {} or A . i = {} )
assume A3: i in I ; ::_thesis: ( not C . i = {} or A . i = {} )
then  ( B . i = {} implies A . i = {} ) by A1, PZFMISC1:def_3;
hence  ( not C . i = {} or A . i = {} ) by A2, A3, PZFMISC1:def_3; ::_thesis: verum
end;

theorem Th11: :: AUTALG_1:11
for x being set
for A being ManySortedSet of {x} holds A = x .--> (A . x)
proof
let x be set ; ::_thesis: for A being ManySortedSet of {x} holds A = x .--> (A . x)
let A be ManySortedSet of {x}; ::_thesis: A = x .--> (A . x)
A1: dom A = {x} by PARTFUN1:def_2;
then  rng A = {(A . x)} by FUNCT_1:4;
hence  A = x .--> (A . x) by A1, FUNCOP_1:9; ::_thesis: verum
end;

theorem Th12: :: AUTALG_1:12
for I being set
for A, B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds
( F "" is "1-1" & F "" is "onto" )
proof
let I be set ; ::_thesis: for A, B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds
( F "" is "1-1" & F "" is "onto" )
let A, B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds
( F "" is "1-1" & F "" is "onto" )
let F be ManySortedFunction of A,B; ::_thesis: ( F is "1-1" & F is "onto" implies ( F "" is "1-1" & F "" is "onto" ) )
assume A1: ( F is "1-1" & F is "onto" ) ; ::_thesis: ( F "" is "1-1" & F "" is "onto" )
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(F_"")_._i_is_one-to-one
let i be set ; ::_thesis: ( i in I implies (F "") . i is one-to-one )
assume A2: i in I ; ::_thesis: (F "") . i is one-to-one
then reconsider g = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
 g is one-to-one by A1, A2, MSUALG_3:1;
then  g " is one-to-one ;
hence  (F "") . i is one-to-one by A1, A2, MSUALG_3:def_4; ::_thesis: verum
end;
hence  F "" is "1-1" by MSUALG_3:1; ::_thesis: F "" is "onto"
thus  F "" is "onto" ::_thesis: verum
proof
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng ((F "") . i) = A . i )
assume A3: i in I ; ::_thesis: rng ((F "") . i) = A . i
then reconsider g = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
A4: g is one-to-one by A1, A3, MSUALG_3:1;
A . i = dom g by A3, FUNCT_2:def_1
.= rng (g ") by A4, FUNCT_1:33 ;
hence  rng ((F "") . i) = A . i by A1, A3, MSUALG_3:def_4; ::_thesis: verum
end;
end;

theorem :: AUTALG_1:13
for I being set
for A, B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds
(F "") "" = F
proof
let I be set ; ::_thesis: for A, B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds
(F "") "" = F
let A, B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds
(F "") "" = F
let F be ManySortedFunction of A,B; ::_thesis: ( F is "1-1" & F is "onto" implies (F "") "" = F )
assume A1: ( F is "1-1" & F is "onto" ) ; ::_thesis: (F "") "" = F
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
((F_"")_"")_._i_=_F_._i
let i be set ; ::_thesis: ( i in I implies ((F "") "") . i = F . i )
assume A2: i in I ; ::_thesis: ((F "") "") . i = F . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
reconsider f9 = (F "") . i as Function of (B . i),(A . i) by A2, PBOOLE:def_15;
 f is one-to-one by A1, A2, MSUALG_3:1;
then A3: (f ") " = f by FUNCT_1:43;
 ( F "" is "1-1" & F "" is "onto" ) by A1, Th12;
then  ((F "") "") . i = f9 " by A2, MSUALG_3:def_4;
hence  ((F "") "") . i = F . i by A1, A2, A3, MSUALG_3:def_4; ::_thesis: verum
end;
hence  (F "") "" = F by PBOOLE:3; ::_thesis: verum
end;

theorem Th14: :: AUTALG_1:14
for F, G being Function-yielding Function st F is "1-1" & G is "1-1" holds
G ** F is "1-1"
proof
let F, G be Function-yielding Function; ::_thesis: ( F is "1-1" & G is "1-1" implies G ** F is "1-1" )
assume that
A1: F is "1-1" and
A2: G is "1-1" ; ::_thesis: G ** F is "1-1"
let i be set ; :: according to MSUALG_3:def_2 ::_thesis: for b1 being set holds
( not i in dom (G ** F) or not (G ** F) . i = b1 or b1 is one-to-one )
let f be Function; ::_thesis: ( not i in dom (G ** F) or not (G ** F) . i = f or f is one-to-one )
assume that
A3: i in dom (G ** F) and
A4: (G ** F) . i = f ; ::_thesis: f is one-to-one
A5: dom (G ** F) = (dom G) /\ (dom F) by PBOOLE:def_19;
then  i in dom F by A3, XBOOLE_0:def_4;
then A6: F . i is one-to-one by A1, MSUALG_3:def_2;
 i in dom G by A3, A5, XBOOLE_0:def_4;
then  G . i is one-to-one by A2, MSUALG_3:def_2;
then  (G . i) * (F . i) is one-to-one by A6;
hence  f is one-to-one by A3, A4, PBOOLE:def_19; ::_thesis: verum
end;

theorem Th15: :: AUTALG_1:15
for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds
G ** F is "onto"
proof
let I be set ; ::_thesis: for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds
G ** F is "onto"
let A be ManySortedSet of I; ::_thesis: for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds
G ** F is "onto"
let B, C be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds
G ** F is "onto"
let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds
G ** F is "onto"
let G be ManySortedFunction of B,C; ::_thesis: ( F is "onto" & G is "onto" implies G ** F is "onto" )
assume A1: ( F is "onto" & G is "onto" ) ; ::_thesis: G ** F is "onto"
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
rng_((G_**_F)_._i)_=_C_._i
let i be set ; ::_thesis: ( i in I implies rng ((G ** F) . i) = C . i )
assume A2: i in I ; ::_thesis: rng ((G ** F) . i) = C . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
reconsider g = G . i as Function of (B . i),(C . i) by A2, PBOOLE:def_15;
 ( rng f = B . i & rng g = C . i ) by A1, A2, MSUALG_3:def_3;
then  rng (g * f) = C . i by A2, FUNCT_2:14;
hence  rng ((G ** F) . i) = C . i by A2, MSUALG_3:2; ::_thesis: verum
end;
hence  G ** F is "onto" by MSUALG_3:def_3; ::_thesis: verum
end;

theorem :: AUTALG_1:16
for I being set
for A, B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds
(G ** F) "" = (F "") ** (G "")
proof
let I be set ; ::_thesis: for A, B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds
(G ** F) "" = (F "") ** (G "")
let A, B, C be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds
(G ** F) "" = (F "") ** (G "")
let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds
(G ** F) "" = (F "") ** (G "")
let G be ManySortedFunction of B,C; ::_thesis: ( F is "1-1" & F is "onto" & G is "1-1" & G is "onto" implies (G ** F) "" = (F "") ** (G "") )
assume that
A1: ( F is "1-1" & F is "onto" ) and
A2: ( G is "1-1" & G is "onto" ) ; ::_thesis: (G ** F) "" = (F "") ** (G "")
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
((G_**_F)_"")_._i_=_((F_"")_**_(G_""))_._i
let i be set ; ::_thesis: ( i in I implies ((G ** F) "") . i = ((F "") ** (G "")) . i )
assume A3: i in I ; ::_thesis: ((G ** F) "") . i = ((F "") ** (G "")) . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
A4: f is one-to-one by A1, A3, MSUALG_3:1;
reconsider g = G . i as Function of (B . i),(C . i) by A3, PBOOLE:def_15;
A5: g is one-to-one by A2, A3, MSUALG_3:1;
 ( (F "") . i = f " & rng f = B . i ) by A1, A3, MSUALG_3:def_3, MSUALG_3:def_4;
then reconsider ff = (F "") . i as Function of (B . i),(A . i) by A4, FUNCT_2:25;
A6: ( G ** F is "1-1" & G ** F is "onto" ) by A1, A2, Th14, Th15;
 (G ** F) . i = g * f by A3, MSUALG_3:2;
then A7: ((G ** F) "") . i = (g * f) " by A3, A6, MSUALG_3:def_4;
 ( (G "") . i = g " & rng g = C . i ) by A2, A3, MSUALG_3:def_3, MSUALG_3:def_4;
then reconsider gg = (G "") . i as Function of (C . i),(B . i) by A5, FUNCT_2:25;
((F "") ** (G "")) . i = ff * gg by A3, MSUALG_3:2
.= ff * (g ") by A2, A3, MSUALG_3:def_4
.= (f ") * (g ") by A1, A3, MSUALG_3:def_4 ;
hence  ((G ** F) "") . i = ((F "") ** (G "")) . i by A4, A5, A7, FUNCT_1:44; ::_thesis: verum
end;
hence  (G ** F) "" = (F "") ** (G "") by PBOOLE:3; ::_thesis: verum
end;

theorem Th17: :: AUTALG_1:17
for I being set
for A, B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds
G = F ""
proof
let I be set ; ::_thesis: for A, B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds
G = F ""
let A, B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds
G = F ""
let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds
G = F ""
let G be ManySortedFunction of B,A; ::_thesis: ( F is "1-1" & F is "onto" & G ** F = id A implies G = F "" )
assume that
A1: F is "1-1" and
A2: F is "onto" and
A3: G ** F = id A ; ::_thesis: G = F ""
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
G_._i_=_(F_"")_._i
let i be set ; ::_thesis: ( i in I implies G . i = (F "") . i )
assume A4: i in I ; ::_thesis: G . i = (F "") . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
A5: f is one-to-one by A1, A4, MSUALG_3:1;
reconsider g = G . i as Function of (B . i),(A . i) by A4, PBOOLE:def_15;
 (G ** F) . i = id (A . i) by A3, A4, MSUALG_3:def_1;
then A6: g * f = id (A . i) by A4, MSUALG_3:2;
 ( (F "") . i = f " & rng f = B . i ) by A1, A2, A4, MSUALG_3:def_3, MSUALG_3:def_4;
hence  G . i = (F "") . i by A4, A6, A5, FUNCT_2:30; ::_thesis: verum
end;
hence  G = F "" by PBOOLE:3; ::_thesis: verum
end;

theorem Th18: :: AUTALG_1:18
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
(Funcs) (A,B) is V2()
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds
(Funcs) (A,B) is V2()
let A, B be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies (Funcs) (A,B) is V2() )
assume A1: A is_transformable_to B ; ::_thesis: (Funcs) (A,B) is V2()
A2: for i being set st i in I holds
Funcs ((A . i),(B . i)) <> {}
proof
let i be set ; ::_thesis: ( i in I implies Funcs ((A . i),(B . i)) <> {} )
assume  i in I ; ::_thesis: Funcs ((A . i),(B . i)) <> {}
then  ( B . i = {} implies A . i = {} ) by A1, PZFMISC1:def_3;
hence  Funcs ((A . i),(B . i)) <> {} by FUNCT_2:8; ::_thesis: verum
end;
 for i being set st i in I holds
((Funcs) (A,B)) . i <> {}
proof
let i be set ; ::_thesis: ( i in I implies ((Funcs) (A,B)) . i <> {} )
assume A3: i in I ; ::_thesis: ((Funcs) (A,B)) . i <> {}
then  ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) by PBOOLE:def_17;
hence  ((Funcs) (A,B)) . i <> {} by A2, A3; ::_thesis: verum
end;
then  for i being set st i in I holds
not ((Funcs) (A,B)) . i is empty ;
hence  (Funcs) (A,B) is V2() by PBOOLE:def_13; ::_thesis: verum
end;

definition
let I be set ;
let A, B be ManySortedSet of I;
assume A1: A is_transformable_to B ;
func MSFuncs (A,B) ->  non empty set  equals :Def4: :: AUTALG_1:def 4
 product ((Funcs) (A,B));
coherence
 product ((Funcs) (A,B)) is non empty set
proof
 (Funcs) (A,B) is V2() by A1, Th18;
then  not {} in rng ((Funcs) (A,B)) by PBOOLE:137;
hence  product ((Funcs) (A,B)) is non empty set by CARD_3:26; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines MSFuncs AUTALG_1:def_4_:_
 for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
MSFuncs (A,B) = product ((Funcs) (A,B));

theorem Th19: :: AUTALG_1:19
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for x being set st x in MSFuncs (A,B) holds
x is ManySortedFunction of A,B
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds
for x being set st x in MSFuncs (A,B) holds
x is ManySortedFunction of A,B
let A, B be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies for x being set st x in MSFuncs (A,B) holds
x is ManySortedFunction of A,B )
assume A1: A is_transformable_to B ; ::_thesis: for x being set st x in MSFuncs (A,B) holds
x is ManySortedFunction of A,B
set f = (Funcs) (A,B);
let x be set ; ::_thesis: ( x in MSFuncs (A,B) implies x is ManySortedFunction of A,B )
assume  x in MSFuncs (A,B) ; ::_thesis: x is ManySortedFunction of A,B
then  x in product ((Funcs) (A,B)) by A1, Def4;
then consider g being Function such that
A2: x = g and
A3: dom g = dom ((Funcs) (A,B)) and
A4: for i being set st i in dom ((Funcs) (A,B)) holds
g . i in ((Funcs) (A,B)) . i by CARD_3:def_5;
A5: dom ((Funcs) (A,B)) = I by PARTFUN1:def_2;
A6: for i being set st i in I holds
g . i in Funcs ((A . i),(B . i))
proof
let i be set ; ::_thesis: ( i in I implies g . i in Funcs ((A . i),(B . i)) )
assume A7: i in I ; ::_thesis: g . i in Funcs ((A . i),(B . i))
then  ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) by PBOOLE:def_17;
hence  g . i in Funcs ((A . i),(B . i)) by A4, A5, A7; ::_thesis: verum
end;
A8: for i being set st i in I holds
ex F being Function st
( F = g . i & dom F = A . i & rng F c= B . i )
proof
let i be set ; ::_thesis: ( i in I implies ex F being Function st
( F = g . i & dom F = A . i & rng F c= B . i ) )
assume  i in I ; ::_thesis: ex F being Function st
( F = g . i & dom F = A . i & rng F c= B . i )
then  g . i in Funcs ((A . i),(B . i)) by A6;
hence  ex F being Function st
( F = g . i & dom F = A . i & rng F c= B . i ) by FUNCT_2:def_2; ::_thesis: verum
end;
A9: for i being set st i in I holds
g . i is Function of (A . i),(B . i)
proof
let i be set ; ::_thesis: ( i in I implies g . i is Function of (A . i),(B . i) )
assume A10: i in I ; ::_thesis: g . i is Function of (A . i),(B . i)
 ex F being Function st
( F = g . i & dom F = A . i & rng F c= B . i ) by A8, A10;
hence  g . i is Function of (A . i),(B . i) by FUNCT_2:2; ::_thesis: verum
end;
 dom g = I by A3, PARTFUN1:def_2;
then  g is ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
hence  x is ManySortedFunction of A,B by A2, A9, PBOOLE:def_15; ::_thesis: verum
end;

theorem Th20: :: AUTALG_1:20
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for g being ManySortedFunction of A,B holds g in MSFuncs (A,B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds
for g being ManySortedFunction of A,B holds g in MSFuncs (A,B)
let A, B be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies for g being ManySortedFunction of A,B holds g in MSFuncs (A,B) )
assume A1: A is_transformable_to B ; ::_thesis: for g being ManySortedFunction of A,B holds g in MSFuncs (A,B)
set f = (Funcs) (A,B);
let g be ManySortedFunction of A,B; ::_thesis: g in MSFuncs (A,B)
A2: dom ((Funcs) (A,B)) = I by PARTFUN1:def_2;
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_((Funcs)_(A,B))_holds_
g_._x_in_((Funcs)_(A,B))_._x
let x be set ; ::_thesis: ( x in dom ((Funcs) (A,B)) implies g . x in ((Funcs) (A,B)) . x )
assume A4: x in dom ((Funcs) (A,B)) ; ::_thesis: g . x in ((Funcs) (A,B)) . x
then reconsider i = x as Element of I by PARTFUN1:def_2;
A5: g . i is Function of (A . i),(B . i) by A2, A4, PBOOLE:def_15;
 ( B . i = {} implies A . i = {} ) by A1, A2, A4, PZFMISC1:def_3;
then  g . i in Funcs ((A . i),(B . i)) by A5, FUNCT_2:8;
hence  g . x in ((Funcs) (A,B)) . x by A2, A4, PBOOLE:def_17; ::_thesis: verum
end;
 dom g = I by PARTFUN1:def_2;
then  g in product ((Funcs) (A,B)) by A2, A3, CARD_3:9;
hence  g in MSFuncs (A,B) by A1, Def4; ::_thesis: verum
end;

registration
let I be set ;
let A be ManySortedSet of I;
cluster (Funcs) (A,A) -> V2() ;
coherence
 (Funcs) (A,A) is non-empty
proof
 for i being set st i in I holds
not ((Funcs) (A,A)) . i is empty
proof
let i be set ; ::_thesis: ( i in I implies not ((Funcs) (A,A)) . i is empty )
assume A1: i in I ; ::_thesis: not ((Funcs) (A,A)) . i is empty
then  (id A) . i is Function of (A . i),(A . i) by PBOOLE:def_15;
then  (id A) . i in Funcs ((A . i),(A . i)) by FUNCT_2:9;
hence  not ((Funcs) (A,A)) . i is empty by A1, PBOOLE:def_17; ::_thesis: verum
end;
hence  (Funcs) (A,A) is non-empty by PBOOLE:def_13; ::_thesis: verum
end;
end;

definition
let I be set ;
let D be ManySortedSet of I;
let A be non empty Subset of (MSFuncs (D,D));
:: original: Element
redefine mode Element of A ->  ManySortedFunction of D,D;
coherence
 for b1 being Element of A holds b1 is ManySortedFunction of D,D
proof
let f be Element of A; ::_thesis: f is ManySortedFunction of D,D
thus  f is ManySortedFunction of D,D by Th19; ::_thesis: verum
end;
end;

registration
let I be set ;
let A be ManySortedSet of I;
cluster id A ->  "onto" ;
coherence
 id A is "onto"
proof
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng ((id A) . i) = A . i )
assume  i in I ; ::_thesis: rng ((id A) . i) = A . i
then  (id A) . i = id (A . i) by MSUALG_3:def_1;
hence  rng ((id A) . i) = A . i by RELAT_1:45; ::_thesis: verum
end;
cluster id A ->  "1-1" ;
coherence
 id A is "1-1"
proof
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(id_A)_._i_is_one-to-one
let i be set ; ::_thesis: ( i in I implies (id A) . i is one-to-one )
assume  i in I ; ::_thesis: (id A) . i is one-to-one
then  (id A) . i = id (A . i) by MSUALG_3:def_1;
hence  (id A) . i is one-to-one ; ::_thesis: verum
end;
hence  id A is "1-1" by MSUALG_3:1; ::_thesis: verum
end;
end;

begin


definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
mode MSFunctionSet of U1,U2 is non empty Subset of (MSFuncs ( the Sorts of U1, the Sorts of U2));
end;

theorem :: AUTALG_1:21
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSFuncs ( the Sorts of U1, the Sorts of U1) by Th20;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
set T = the Sorts of U1;
func MSAAut U1 ->  MSFunctionSet of U1,U1 means :Def5: :: AUTALG_1:def 5
 for h being ManySortedFunction of U1,U1 holds
( h in it iff h is_isomorphism U1,U1 );
existence
 ex b1 being MSFunctionSet of U1,U1 st
for h being ManySortedFunction of U1,U1 holds
( h in b1 iff h is_isomorphism U1,U1 )
proof
defpred S1[ set ] means  ex msf being ManySortedFunction of U1,U1 st
( $1 = msf & msf is_isomorphism 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();
A2: X c= MSFuncs ( the Sorts of U1, the Sorts of U1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in MSFuncs ( the Sorts of U1, the Sorts of U1) )
thus  ( not x in X or x in MSFuncs ( the Sorts of U1, the Sorts of U1) ) by A1; ::_thesis: verum
end;
 ( 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_isomorphism U1,U1 ) ) by Th20, MSUALG_3:16;
then reconsider X = X as MSFunctionSet of U1,U1 by A1, A2;
take  X ; ::_thesis: for h being ManySortedFunction of U1,U1 holds
( h in X iff h is_isomorphism U1,U1 )
let h be ManySortedFunction of U1,U1; ::_thesis: ( h in X iff h is_isomorphism U1,U1 )
hereby  ::_thesis: ( h is_isomorphism U1,U1 implies h in X )
assume  h in X ; ::_thesis: h is_isomorphism U1,U1
then  ex msf being ManySortedFunction of U1,U1 st
( h = msf & msf is_isomorphism U1,U1 ) by A1;
hence  h is_isomorphism U1,U1 ; ::_thesis: verum
end;
 h in MSFuncs ( the Sorts of U1, the Sorts of U1) by Th20;
hence  ( h is_isomorphism U1,U1 implies h in X ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being MSFunctionSet of U1,U1 st ( for h being ManySortedFunction of U1,U1 holds
( h in b1 iff h is_isomorphism U1,U1 ) ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b2 iff h is_isomorphism U1,U1 ) ) holds
b1 = b2
proof
let F1, F2 be MSFunctionSet of U1,U1; ::_thesis: ( ( for h being ManySortedFunction of U1,U1 holds
( h in F1 iff h is_isomorphism U1,U1 ) ) & ( for h being ManySortedFunction of U1,U1 holds
( h in F2 iff h is_isomorphism U1,U1 ) ) implies F1 = F2 )
assume that
A3: for h being ManySortedFunction of U1,U1 holds
( h in F1 iff h is_isomorphism U1,U1 ) and
A4: for h being ManySortedFunction of U1,U1 holds
( h in F2 iff h is_isomorphism U1,U1 ) ; ::_thesis: F1 = F2
thus  F1 c= F2 :: according to XBOOLE_0:def_10 ::_thesis: F2 c= F1
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F1 or q in F2 )
assume A5: q in F1 ; ::_thesis: q in F2
then reconsider h1 = q as ManySortedFunction of U1,U1 by Th19;
 h1 is_isomorphism U1,U1 by A3, A5;
hence  q in F2 by A4; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F2 or q in F1 )
assume A6: q in F2 ; ::_thesis: q in F1
then reconsider h1 = q as ManySortedFunction of U1,U1 by Th19;
 h1 is_isomorphism U1,U1 by A4, A6;
hence  q in F1 by A3; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines MSAAut AUTALG_1:def_5_:_
 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 = MSAAut U1 iff for h being ManySortedFunction of U1,U1 holds
( h in b3 iff h is_isomorphism U1,U1 ) );

theorem :: AUTALG_1:22
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for f being Element of MSAAut U1 holds f in MSFuncs ( the Sorts of U1, the Sorts of U1) by Th20;

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

Lm3:  for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for f being Element of MSAAut U1 holds
( f is "1-1" & f is "onto" )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S
for f being Element of MSAAut U1 holds
( f is "1-1" & f is "onto" )
let U1 be non-empty MSAlgebra over S; ::_thesis: for f being Element of MSAAut U1 holds
( f is "1-1" & f is "onto" )
let f be Element of MSAAut U1; ::_thesis: ( f is "1-1" & f is "onto" )
 f is_isomorphism U1,U1 by Def5;
hence  ( f is "1-1" & f is "onto" ) by MSUALG_3:13; ::_thesis: verum
end;

theorem Th24: :: AUTALG_1:24
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSAAut 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 MSAAut U1
let U1 be non-empty MSAlgebra over S; ::_thesis: id the Sorts of U1 in MSAAut U1
 id the Sorts of U1 is_isomorphism U1,U1 by MSUALG_3:16;
hence  id the Sorts of U1 in MSAAut U1 by Def5; ::_thesis: verum
end;

theorem Th25: :: AUTALG_1:25
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for f being Element of MSAAut U1 holds f "" in MSAAut U1
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S
for f being Element of MSAAut U1 holds f "" in MSAAut U1
let U1 be non-empty MSAlgebra over S; ::_thesis: for f being Element of MSAAut U1 holds f "" in MSAAut U1
let f be Element of MSAAut U1; ::_thesis: f "" in MSAAut U1
 f is_isomorphism U1,U1 by Def5;
then  f "" is_isomorphism U1,U1 by MSUALG_3:14;
hence  f "" in MSAAut U1 by Def5; ::_thesis: verum
end;

theorem Th26: :: AUTALG_1:26
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for f1, f2 being Element of MSAAut U1 holds f1 ** f2 in MSAAut 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 MSAAut U1 holds f1 ** f2 in MSAAut U1
let U1 be non-empty MSAlgebra over S; ::_thesis: for f1, f2 being Element of MSAAut U1 holds f1 ** f2 in MSAAut U1
let f1, f2 be Element of MSAAut U1; ::_thesis: f1 ** f2 in MSAAut U1
 ( f1 is_isomorphism U1,U1 & f2 is_isomorphism U1,U1 ) by Def5;
then  f1 ** f2 is_isomorphism U1,U1 by MSUALG_3:15;
hence  f1 ** f2 in MSAAut U1 by Def5; ::_thesis: verum
end;

theorem Th27: :: AUTALG_1:27
for UA being Universal_Algebra
for F being ManySortedFunction of (MSAlg UA),(MSAlg UA)
for f being Element of UAAut UA st F = 0 .--> f holds
F in MSAAut (MSAlg UA)
proof
let UA be Universal_Algebra; ::_thesis: for F being ManySortedFunction of (MSAlg UA),(MSAlg UA)
for f being Element of UAAut UA st F = 0 .--> f holds
F in MSAAut (MSAlg UA)
let F be ManySortedFunction of (MSAlg UA),(MSAlg UA); ::_thesis: for f being Element of UAAut UA st F = 0 .--> f holds
F in MSAAut (MSAlg UA)
let f be Element of UAAut UA; ::_thesis: ( F = 0 .--> f implies F in MSAAut (MSAlg UA) )
assume  F = 0 .--> f ; ::_thesis: F in MSAAut (MSAlg UA)
then A1: F = MSAlg f by MSUHOM_1:def_3;
 f is_isomorphism UA,UA by Def1;
then  MSAlg f is_isomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:20;
then  F is_isomorphism MSAlg UA, MSAlg UA by A1, MSUHOM_1:9;
hence  F in MSAAut (MSAlg UA) by Def5; ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
func MSAAutComp U1 ->  BinOp of (MSAAut U1) means :Def6: :: AUTALG_1:def 6
 for x, y being Element of MSAAut U1 holds it . (x,y) = y ** x;
existence
 ex b1 being BinOp of (MSAAut U1) st
for x, y being Element of MSAAut U1 holds b1 . (x,y) = y ** x
proof
defpred S1[ Element of MSAAut U1, Element of MSAAut U1, set ] means $3 = $2 ** $1;
A1: for x, y being Element of MSAAut U1 ex m being Element of MSAAut U1 st S1[x,y,m]
proof
let x, y be Element of MSAAut U1; ::_thesis: ex m being Element of MSAAut U1 st S1[x,y,m]
reconsider xx = x, yy = y as ManySortedFunction of U1,U1 ;
reconsider m = yy ** xx as Element of MSAAut U1 by Th26;
take  m ; ::_thesis: S1[x,y,m]
thus  S1[x,y,m] ; ::_thesis: verum
end;
thus  ex IT being BinOp of (MSAAut U1) st
for x, y being Element of MSAAut U1 holds S1[x,y,IT . (x,y)] from BINOP_1:sch_3(A1); ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (MSAAut U1) st ( for x, y being Element of MSAAut U1 holds b1 . (x,y) = y ** x ) & ( for x, y being Element of MSAAut U1 holds b2 . (x,y) = y ** x ) holds
b1 = b2
proof
let b1, b2 be BinOp of (MSAAut U1); ::_thesis: ( ( for x, y being Element of MSAAut U1 holds b1 . (x,y) = y ** x ) & ( for x, y being Element of MSAAut U1 holds b2 . (x,y) = y ** x ) implies b1 = b2 )
assume that
A2: for x, y being Element of MSAAut U1 holds b1 . (x,y) = y ** x and
A3: for x, y being Element of MSAAut U1 holds b2 . (x,y) = y ** x ; ::_thesis: b1 = b2
 for x, y being Element of MSAAut U1 holds b1 . (x,y) = b2 . (x,y)
proof
let x, y be Element of MSAAut 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 Def6 defines MSAAutComp AUTALG_1:def_6_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for b3 being BinOp of (MSAAut U1) holds
( b3 = MSAAutComp U1 iff for x, y being Element of MSAAut 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 MSAAutGroup U1 ->  Group equals :: AUTALG_1:def 7
 multMagma(# (MSAAut U1),(MSAAutComp U1) #);
coherence
 multMagma(# (MSAAut U1),(MSAAutComp U1) #) is Group
proof
set SO = the Sorts of U1;
set H = multMagma(# (MSAAut U1),(MSAAutComp U1) #);
A1: ex e being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st
for h being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st
( h * g = e & g * h = e ) )
proof
reconsider e = id the Sorts of U1 as Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) by Th24;
take  e ; ::_thesis: for h being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st
( h * g = e & g * h = e ) )
let h be Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #); ::_thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st
( h * g = e & g * h = e ) )
consider A being Element of MSAAut U1 such that
A2: A = h ;
h * e = (id the Sorts of U1) ** A by A2, Def6
.= A by MSUALG_3:4 ;
hence  h * e = h by A2; ::_thesis: ( e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st
( h * g = e & g * h = e ) )
e * h = A ** (id the Sorts of U1) by A2, Def6
.= A by MSUALG_3:3 ;
hence  e * h = h by A2; ::_thesis: ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st
( h * g = e & g * h = e )
reconsider g = A "" as Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) by Th25;
take  g ; ::_thesis: ( h * g = e & g * h = e )
A3: ( A is "onto" & A is "1-1" ) by Lm3;
thus h * g = (A "") ** A by A2, Def6
.= e by A3, MSUALG_3:5 ; ::_thesis: g * h = e
thus g * h = A ** (A "") by A2, Def6
.= e by A3, MSUALG_3:5 ; ::_thesis: verum
end;
 for f, g, h being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) holds (f * g) * h = f * (g * h)
proof
let f, g, h be Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #); ::_thesis: (f * g) * h = f * (g * h)
reconsider A = f, B = g, C = h as Element of MSAAut U1 ;
A4: g * h = C ** B by Def6;
 f * g = B ** A by Def6;
hence (f * g) * h = C ** (B ** A) by Def6
.= (C ** B) ** A by PBOOLE:140
.= f * (g * h) by A4, Def6 ;
::_thesis: verum
end;
hence  multMagma(# (MSAAut U1),(MSAAutComp U1) #) is Group by A1, GROUP_1:def_2, GROUP_1:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines MSAAutGroup AUTALG_1:def_7_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds MSAAutGroup U1 = multMagma(# (MSAAut U1),(MSAAutComp U1) #);

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
cluster MSAAutGroup U1 ->  strict ;
coherence
 MSAAutGroup U1 is strict ;
end;

theorem :: AUTALG_1:28
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for x, y being Element of (MSAAutGroup U1)
for f, g being Element of MSAAut U1 st x = f & y = g holds
x * y = g ** f by Def6;

theorem Th29: :: AUTALG_1:29
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 = 1_ (MSAAutGroup 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 = 1_ (MSAAutGroup U1)
let U1 be non-empty MSAlgebra over S; ::_thesis: id the Sorts of U1 = 1_ (MSAAutGroup U1)
set T = the Sorts of U1;
set f = the Element of (MSAAutGroup U1);
reconsider g = id the Sorts of U1 as Element of (MSAAutGroup U1) by Th24;
consider g1 being ManySortedFunction of the Sorts of U1, the Sorts of U1 such that
A1: g1 = g ;
 the Element of (MSAAutGroup U1) is Element of MSAAut U1 ;
then consider f1 being ManySortedFunction of the Sorts of U1, the Sorts of U1 such that
A2: f1 = the Element of (MSAAutGroup U1) ;
g * the Element of (MSAAutGroup U1) = f1 ** g1 by A1, A2, Def6
.= the Element of (MSAAutGroup U1) by A1, A2, MSUALG_3:3 ;
hence  id the Sorts of U1 = 1_ (MSAAutGroup U1) by GROUP_1:7; ::_thesis: verum
end;

theorem :: AUTALG_1:30
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for f being Element of MSAAut U1
for g being Element of (MSAAutGroup U1) st f = g holds
f "" = g "
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S
for f being Element of MSAAut U1
for g being Element of (MSAAutGroup U1) st f = g holds
f "" = g "
let U1 be non-empty MSAlgebra over S; ::_thesis: for f being Element of MSAAut U1
for g being Element of (MSAAutGroup U1) st f = g holds
f "" = g "
let f be Element of MSAAut U1; ::_thesis: for g being Element of (MSAAutGroup U1) st f = g holds
f "" = g "
let g be Element of (MSAAutGroup U1); ::_thesis: ( f = g implies f "" = g " )
consider g1 being Element of MSAAut U1 such that
A1: g1 = g " ;
assume  f = g ; ::_thesis: f "" = g "
then  g1 ** f = g * (g ") by A1, Def6;
then  g1 ** f = 1_ (MSAAutGroup U1) by GROUP_1:def_5;
then A2: g1 ** f = id the Sorts of U1 by Th29;
 ( f is "1-1" & f is "onto" ) by Lm3;
hence  f "" = g " by A1, A2, Th17; ::_thesis: verum
end;

begin

theorem Th31: :: AUTALG_1:31
for UA1, UA2 being Universal_Algebra st UA1,UA2 are_similar holds
for F being ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)) holds F . 0 is Function of UA1,UA2
proof
let UA1, UA2 be Universal_Algebra; ::_thesis: ( UA1,UA2 are_similar implies for F being ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)) holds F . 0 is Function of UA1,UA2 )
A1: 0 in {0} by TARSKI:def_1;
assume  UA1,UA2 are_similar ; ::_thesis: for F being ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)) holds F . 0 is Function of UA1,UA2
then  MSSign UA1 = MSSign UA2 by MSUHOM_1:10;
then A2: ( MSAlg UA2 = MSAlgebra(# (MSSorts UA2),(MSCharact UA2) #) & (MSAlg UA2) Over (MSSign UA1) = MSAlg UA2 ) by MSUALG_1:def_11, MSUHOM_1:9;
let F be ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)); ::_thesis: F . 0 is Function of UA1,UA2
A3: ( the carrier of (MSSign UA1) = {0} & MSAlg UA1 = MSAlgebra(# (MSSorts UA1),(MSCharact UA1) #) ) by MSUALG_1:def_8, MSUALG_1:def_11;
A4: (MSSorts UA2) . 0 = (0 .--> the carrier of UA2) . 0 by MSUALG_1:def_9
.= the carrier of UA2 by A1, FUNCOP_1:7 ;
(MSSorts UA1) . 0 = (0 .--> the carrier of UA1) . 0 by MSUALG_1:def_9
.= the carrier of UA1 by A1, FUNCOP_1:7 ;
hence  F . 0 is Function of UA1,UA2 by A1, A3, A4, A2, PBOOLE:def_15; ::_thesis: verum
end;

theorem Th32: :: AUTALG_1:32
for UA being Universal_Algebra
for f being Element of UAAut UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)
proof
let UA be Universal_Algebra; ::_thesis: for f being Element of UAAut UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)
let f be Element of UAAut 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;

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)
proof
let UA be Universal_Algebra; ::_thesis: 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)
let h be Function; ::_thesis: ( dom h = UAAut UA & ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) implies rng h = MSAAut (MSAlg UA) )
assume that
A1: dom h = UAAut UA and
A2: for x being set st x in UAAut UA holds
h . x = 0 .--> x ; ::_thesis: rng h = MSAAut (MSAlg UA)
thus  rng h c= MSAAut (MSAlg UA) :: according to XBOOLE_0:def_10 ::_thesis: MSAAut (MSAlg UA) c= rng h
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng h or x in MSAAut (MSAlg UA) )
assume  x in rng h ; ::_thesis: x in MSAAut (MSAlg UA)
then consider q being set  such that
A3: q in dom h and
A4: x = h . q by FUNCT_1:def_3;
consider q9 being Element of UAAut UA such that
A5: q9 = q by A1, A3;
 ( x = 0 .--> q & 0 .--> q is ManySortedFunction of (MSAlg UA),(MSAlg UA) ) by A1, A2, A3, A4, Th32;
then consider d being ManySortedFunction of (MSAlg UA),(MSAlg UA) such that
A6: d = x ;
 q9 is_isomorphism UA,UA by Def1;
then A7: MSAlg q9 is_isomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:20;
MSAlg q9 = 0 .--> q by A5, MSUHOM_1:def_3
.= x by A1, A2, A3, A4 ;
then  d is_isomorphism MSAlg UA, MSAlg UA by A6, A7, MSUHOM_1:9;
hence  x in MSAAut (MSAlg UA) by A6, Def5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MSAAut (MSAlg UA) or x in rng h )
assume A8: x in MSAAut (MSAlg UA) ; ::_thesis: x in rng h
then reconsider f = x as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Th19;
 the carrier of (MSSign UA) = {0} by MSUALG_1:def_8;
then A9: f = 0 .--> (f . 0) by Th11;
A10: f is_isomorphism MSAlg UA, MSAlg UA by A8, Def5;
 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 Th31;
 MSAlg q9 = f by A9, MSUHOM_1:def_3;
then  MSAlg q9 is_isomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by A10, MSUHOM_1:9;
then  q9 is_isomorphism UA,UA by MSUHOM_1:24;
hence  q in dom h by A1, Def1; ::_thesis: x = h . q
hence  x = h . q by A1, A2, A9; ::_thesis: verum
end;
hence  x in rng h by FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th33: :: AUTALG_1:33
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
h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA))
proof
let UA be Universal_Algebra; ::_thesis: for h being Function st dom h = UAAut UA & ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) holds
h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA))
let h be Function; ::_thesis: ( dom h = UAAut UA & ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) implies h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) )
assume that
A1: dom h = UAAut UA and
A2: for x being set st x in UAAut UA holds
h . x = 0 .--> x ; ::_thesis: h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA))
set H = MSAAutGroup (MSAlg UA);
set G = UAAutGroup UA;
 rng h c= the carrier of (MSAAutGroup (MSAlg UA)) by A1, A2, Lm4;
then reconsider h9 = h as Function of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) by A1, FUNCT_2:def_1, RELSET_1:4;
now__::_thesis:_for_a,_b_being_Element_of_(UAAutGroup_UA)_holds_h9_._(a_*_b)_=_(h9_._a)_*_(h9_._b)
let a, b be Element of (UAAutGroup UA); ::_thesis: h9 . (a * b) = (h9 . a) * (h9 . b)
thus  h9 . (a * b) = (h9 . a) * (h9 . b) ::_thesis: verum
proof
reconsider a9 = a, b9 = b as Element of UAAut UA ;
A3: h9 . (b9 * a9) = 0 .--> (b9 * a9) by A2, Th6;
reconsider A = 0 .--> a9, B = 0 .--> b9 as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Th32;
reconsider ha = h9 . a, hb = h9 . b as Element of MSAAut (MSAlg UA) ;
reconsider A9 = A, B9 = B as Element of (MSAAutGroup (MSAlg UA)) by Th27;
A4: ( ha = A9 & hb = B9 ) by A2;
thus h9 . (a * b) = h9 . (b9 * a9) by Def2
.= MSAlg (b9 * a9) by A3, 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 A4, Def6 ; ::_thesis: verum
end;
end;
hence  h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) by GROUP_6:def_6; ::_thesis: verum
end;

theorem Th34: :: AUTALG_1:34
for UA being Universal_Algebra
for h being Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) st ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) holds
h is bijective
proof
let UA be Universal_Algebra; ::_thesis: for h being Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) st ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) holds
h is bijective
let h be Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)); ::_thesis: ( ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) implies h is bijective )
set G = UAAutGroup UA;
assume A1: for x being set st x in UAAut UA holds
h . x = 0 .--> x ; ::_thesis: h is bijective
 for a, b being Element of (UAAutGroup UA) st h . a = h . b holds
a = b
proof
let a, b be Element of (UAAutGroup UA); ::_thesis: ( h . a = h . b implies a = b )
assume A2: h . a = h . b ; ::_thesis: a = b
A3: h . b = 0 .--> b by A1
.= [:{0},{b}:] ;
h . a = 0 .--> a by A1
.= [:{0},{a}:] ;
then  {a} = {b} by A2, A3, ZFMISC_1:110;
hence  a = b by ZFMISC_1:3; ::_thesis: verum
end;
then A4: h is one-to-one by GROUP_6:1;
 dom h = UAAut UA by FUNCT_2:def_1;
then  rng h = the carrier of (MSAAutGroup (MSAlg UA)) by A1, Lm4;
then  h is onto by FUNCT_2:def_3;
hence  h is bijective by A4; ::_thesis: verum
end;

theorem :: AUTALG_1:35
for UA being Universal_Algebra holds UAAutGroup UA, MSAAutGroup (MSAlg UA) are_isomorphic
proof
let UA be Universal_Algebra; ::_thesis: UAAutGroup UA, MSAAutGroup (MSAlg UA) are_isomorphic
deffunc H1( set ) ->  set = 0 .--> $1;
consider h being Function such that
A1: ( dom h = UAAut UA & ( for x being set st x in UAAut UA holds
h . x = H1(x) ) ) from FUNCT_1:sch_3();
reconsider h = h as Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) by A1, Th33;
take  h ; :: according to GROUP_6:def_11 ::_thesis: h is bijective
thus  h is bijective by A1, Th34; ::_thesis: verum
end;