:: AUTGROUP semantic presentation

begin

          Lm1:  for G being strict Group
for H being Subgroup of G st ( for a, b being Element of G st b is Element of H holds
b |^ a in H ) holds
H is normal
proof
let G be strict Group; ::_thesis: for H being Subgroup of G st ( for a, b being Element of G st b is Element of H holds
b |^ a in H ) holds
H is normal
let H be Subgroup of G; ::_thesis: ( ( for a, b being Element of G st b is Element of H holds
b |^ a in H ) implies H is normal )
assume A1: for a, b being Element of G st b is Element of H holds
b |^ a in H ; ::_thesis: H is normal
now__::_thesis:_for_a_being_Element_of_G_holds_H_*_a_c=_a_*_H
let a be Element of G; ::_thesis: H * a c= a * H
thus  H * a c= a * H ::_thesis: verum
proof
set A = carr H;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in H * a or q in a * H )
assume  q in H * a ; ::_thesis: q in a * H
then consider b being Element of G such that
A2: q = b * a and
A3: b in H by GROUP_2:104;
 b is Element of H by A3, STRUCT_0:def_5;
then  b |^ a in H by A1;
then  b |^ a in carr H by STRUCT_0:def_5;
then  a * (((a ") * b) * a) in a * (carr H) by GROUP_2:27;
then  a * ((a ") * (b * a)) in a * (carr H) by GROUP_1:def_3;
then  (a * (a ")) * (b * a) in a * (carr H) by GROUP_1:def_3;
then  ((a * (a ")) * b) * a in a * (carr H) by GROUP_1:def_3;
then  ((1_ G) * b) * a in a * (carr H) by GROUP_1:def_5;
hence  q in a * H by A2, GROUP_1:def_4; ::_thesis: verum
end;
end;
hence  H is normal by GROUP_3:119; ::_thesis: verum
end;

Lm2:  for G being strict Group
for H being Subgroup of G st H is normal holds
for a, b being Element of G st b is Element of H holds
b |^ a in H
proof
let G be strict Group; ::_thesis: for H being Subgroup of G st H is normal holds
for a, b being Element of G st b is Element of H holds
b |^ a in H
let H be Subgroup of G; ::_thesis: ( H is normal implies for a, b being Element of G st b is Element of H holds
b |^ a in H )
assume A1: H is normal ; ::_thesis: for a, b being Element of G st b is Element of H holds
b |^ a in H
set A = carr H;
let a, b be Element of G; ::_thesis: ( b is Element of H implies b |^ a in H )
 H * a = a * H by A1, GROUP_3:117;
then  ((a ") * H) * a = (a ") * (a * H) by GROUP_2:106;
then  ((a ") * H) * a = ((a ") * a) * H by GROUP_2:105;
then  ((a ") * H) * a = (1_ G) * H by GROUP_1:def_5;
then  ((a ") * H) * a = carr H by GROUP_2:109;
then  the carrier of (H |^ a) = carr H by GROUP_3:59;
then A2: (carr H) |^ a = carr H by GROUP_3:def_6;
assume  b is Element of H ; ::_thesis: b |^ a in H
then  (a ") * b in (a ") * (carr H) by GROUP_2:27;
then  ((a ") * b) * a in ((a ") * (carr H)) * a by GROUP_2:28;
then  b |^ a in carr H by A2, GROUP_3:50;
hence  b |^ a in H by STRUCT_0:def_5; ::_thesis: verum
end;

theorem :: AUTGROUP:1
for G being strict Group
for H being Subgroup of G holds
( ( for a, b being Element of G st b is Element of H holds
b |^ a in H ) iff H is normal ) by Lm1, Lm2;

definition
let G be strict Group;
func Aut G ->  FUNCTION_DOMAIN of the carrier of G, the carrier of G means :Def1: :: AUTGROUP:def 1
( ( for f being Element of it holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in it iff ( h is one-to-one & h is onto ) ) ) );
existence
 ex b1 being FUNCTION_DOMAIN of the carrier of G, the carrier of G st
( ( for f being Element of b1 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b1 iff ( h is one-to-one & h is onto ) ) ) )
proof
set X =  {  x where x is Element of Funcs ( the carrier of G, the carrier of G) : ex h being Homomorphism of G,G st
( x = h & h is one-to-one & h is onto )  }  ;
A1: id the carrier of G in  {  x where x is Element of Funcs ( the carrier of G, the carrier of G) : ex h being Homomorphism of G,G st
( x = h & h is one-to-one & h is onto )  }
proof
set I = id the carrier of G;
A2: id the carrier of G in Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
reconsider I = id the carrier of G as Homomorphism of G,G by GROUP_6:38;
 rng I = the carrier of G by RELAT_1:45;
then  I is onto by FUNCT_2:def_3;
hence  id the carrier of G in  {  x where x is Element of Funcs ( the carrier of G, the carrier of G) : ex h being Homomorphism of G,G st
( x = h & h is one-to-one & h is onto )  }  by A2; ::_thesis: verum
end;
reconsider X =  {  x where x is Element of Funcs ( the carrier of G, the carrier of G) : ex h being Homomorphism of G,G st
( x = h & h is one-to-one & h is onto )  }  as set ;
 X is functional
proof
let q be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not q in X or q is set )
assume  q in X ; ::_thesis: q is set
then  ex x being Element of Funcs ( the carrier of G, the carrier of G) st
( q = x & ex h being Homomorphism of G,G st
( h = x & h is one-to-one & h is onto ) ) ;
hence  q is set ; ::_thesis: verum
end;
then reconsider X = X as functional non empty set by A1;
 X is FUNCTION_DOMAIN of the carrier of G, the carrier of G
proof
let a be Element of X; :: according to FUNCT_2:def_12 ::_thesis: a is Element of bool [: the carrier of G, the carrier of G:]
 a in X ;
then  ex x being Element of Funcs ( the carrier of G, the carrier of G) st
( a = x & ex h being Homomorphism of G,G st
( h = x & h is one-to-one & h is onto ) ) ;
hence  a is Element of bool [: the carrier of G, the carrier of G:] ; ::_thesis: verum
end;
then reconsider X = X as FUNCTION_DOMAIN of the carrier of G, the carrier of G ;
take  X ; ::_thesis: ( ( for f being Element of X holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in X iff ( h is one-to-one & h is onto ) ) ) )
hereby  ::_thesis: for h being Homomorphism of G,G holds
( h in X iff ( h is one-to-one & h is onto ) )
let f be Element of X; ::_thesis: f is Homomorphism of G,G
 f in X ;
then  ex x being Element of Funcs ( the carrier of G, the carrier of G) st
( f = x & ex h being Homomorphism of G,G st
( h = x & h is one-to-one & h is onto ) ) ;
hence  f is Homomorphism of G,G ; ::_thesis: verum
end;
let x be Homomorphism of G,G; ::_thesis: ( x in X iff ( x is one-to-one & x is onto ) )
hereby  ::_thesis: ( x is one-to-one & x is onto implies x in X )
assume  x in X ; ::_thesis: ( x is one-to-one & x is onto )
then  ex f being Element of Funcs ( the carrier of G, the carrier of G) st
( f = x & ex h being Homomorphism of G,G st
( h = f & h is one-to-one & h is onto ) ) ;
hence  ( x is one-to-one & x is onto ) ; ::_thesis: verum
end;
A3: x is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
assume  ( x is one-to-one & x is onto ) ; ::_thesis: x in X
hence  x in X by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FUNCTION_DOMAIN of the carrier of G, the carrier of G st ( for f being Element of b1 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b1 iff ( h is one-to-one & h is onto ) ) ) & ( for f being Element of b2 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b2 iff ( h is one-to-one & h is onto ) ) ) holds
b1 = b2
proof
let F1, F2 be FUNCTION_DOMAIN of the carrier of G, the carrier of G; ::_thesis: ( ( for f being Element of F1 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in F1 iff ( h is one-to-one & h is onto ) ) ) & ( for f being Element of F2 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in F2 iff ( h is one-to-one & h is onto ) ) ) implies F1 = F2 )
assume that
A4: for f being Element of F1 holds f is Homomorphism of G,G and
A5: for h being Homomorphism of G,G holds
( h in F1 iff ( h is one-to-one & h is onto ) ) and
A6: for f being Element of F2 holds f is Homomorphism of G,G and
A7: for h being Homomorphism of G,G holds
( h in F2 iff ( h is one-to-one & h is onto ) ) ; ::_thesis: F1 = F2
A8: F2 c= F1
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F2 or q in F1 )
assume A9: q in F2 ; ::_thesis: q in F1
then reconsider h1 = q as Homomorphism of G,G by A6;
 ( h1 is one-to-one & h1 is onto ) by A7, A9;
hence  q in F1 by A5; ::_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 A10: q in F1 ; ::_thesis: q in F2
then reconsider h1 = q as Homomorphism of G,G by A4;
 ( h1 is one-to-one & h1 is onto ) by A5, A10;
hence  q in F2 by A7; ::_thesis: verum
end;
hence  F1 = F2 by A8, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Aut AUTGROUP:def_1_:_
 for G being strict Group
for b2 being FUNCTION_DOMAIN of the carrier of G, the carrier of G holds
( b2 = Aut G iff ( ( for f being Element of b2 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b2 iff ( h is one-to-one & h is onto ) ) ) ) );

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

theorem Th3: :: AUTGROUP:3
for G being strict Group holds id the carrier of G is Element of Aut G
proof
let G be strict Group; ::_thesis: id the carrier of G is Element of Aut G
 id the carrier of G is Homomorphism of G,G by GROUP_6:38;
then consider h being Homomorphism of G,G such that
A1: h = id the carrier of G ;
 rng h = the carrier of G by A1, RELAT_1:45;
then  h is onto by FUNCT_2:def_3;
hence  id the carrier of G is Element of Aut G by A1, Def1; ::_thesis: verum
end;

theorem Th4: :: AUTGROUP:4
for G being strict Group
for h being Homomorphism of G,G holds
( h in Aut G iff h is bijective )
proof
let G be strict Group; ::_thesis: for h being Homomorphism of G,G holds
( h in Aut G iff h is bijective )
let h be Homomorphism of G,G; ::_thesis: ( h in Aut G iff h is bijective )
hereby  ::_thesis: ( h is bijective implies h in Aut G )
assume  h in Aut G ; ::_thesis: h is bijective
then  ( h is onto & h is one-to-one ) by Def1;
hence  h is bijective ; ::_thesis: verum
end;
thus  ( h is bijective implies h in Aut G ) by Def1; ::_thesis: verum
end;

Lm3:  for G being strict Group
for f being Element of Aut G holds
( dom f = rng f & dom f = the carrier of G )
proof
let G be strict Group; ::_thesis: for f being Element of Aut G holds
( dom f = rng f & dom f = the carrier of G )
let f be Element of Aut G; ::_thesis: ( dom f = rng f & dom f = the carrier of G )
reconsider f = f as Homomorphism of G,G by Def1;
A1: f is bijective by Th4;
then  dom f = the carrier of G by GROUP_6:61;
hence  ( dom f = rng f & dom f = the carrier of G ) by A1, GROUP_6:61; ::_thesis: verum
end;

theorem Th5: :: AUTGROUP:5
for G being strict Group
for f being Element of Aut G holds f " is Homomorphism of G,G
proof
let G be strict Group; ::_thesis: for f being Element of Aut G holds f " is Homomorphism of G,G
let f be Element of Aut G; ::_thesis: f " is Homomorphism of G,G
reconsider f = f as Homomorphism of G,G by Def1;
 f is bijective by Th4;
hence  f " is Homomorphism of G,G by GROUP_6:62; ::_thesis: verum
end;

theorem Th6: :: AUTGROUP:6
for G being strict Group
for f being Element of Aut G holds f " is Element of Aut G
proof
let G be strict Group; ::_thesis: for f being Element of Aut G holds f " is Element of Aut G
let f be Element of Aut G; ::_thesis: f " is Element of Aut G
reconsider f = f as Homomorphism of G,G by Def1;
reconsider A = f " as Homomorphism of G,G by Th5;
 f is bijective by Th4;
then  A is bijective by GROUP_6:63;
hence  f " is Element of Aut G by Def1; ::_thesis: verum
end;

theorem Th7: :: AUTGROUP:7
for G being strict Group
for f1, f2 being Element of Aut G holds f1 * f2 is Element of Aut G
proof
let G be strict Group; ::_thesis: for f1, f2 being Element of Aut G holds f1 * f2 is Element of Aut G
let f1, f2 be Element of Aut G; ::_thesis: f1 * f2 is Element of Aut G
reconsider f1 = f1, f2 = f2 as Homomorphism of G,G by Def1;
 ( f1 is bijective & f2 is bijective ) by Th4;
then  f1 * f2 is bijective ;
hence  f1 * f2 is Element of Aut G by Th4; ::_thesis: verum
end;

definition
let G be strict Group;
func AutComp G ->  BinOp of (Aut G) means :Def2: :: AUTGROUP:def 2
 for x, y being Element of Aut G holds it . (x,y) = x * y;
existence
 ex b1 being BinOp of (Aut G) st
for x, y being Element of Aut G holds b1 . (x,y) = x * y
proof
defpred S1[ Element of Aut G, Element of Aut G, set ] means $3 = $1 * $2;
A1: for x, y being Element of Aut G ex m being Element of Aut G st S1[x,y,m]
proof
let x, y be Element of Aut G; ::_thesis: ex m being Element of Aut G st S1[x,y,m]
reconsider xx = x, yy = y as Homomorphism of G,G by Def1;
reconsider m = xx * yy as Element of Aut G by Th7;
take  m ; ::_thesis: S1[x,y,m]
thus  S1[x,y,m] ; ::_thesis: verum
end;
thus  ex M being BinOp of (Aut G) st
for x, y being Element of Aut G holds S1[x,y,M . (x,y)] from BINOP_1:sch_3(A1); ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Aut G) st ( for x, y being Element of Aut G holds b1 . (x,y) = x * y ) & ( for x, y being Element of Aut G holds b2 . (x,y) = x * y ) holds
b1 = b2
proof
let b1, b2 be BinOp of (Aut G); ::_thesis: ( ( for x, y being Element of Aut G holds b1 . (x,y) = x * y ) & ( for x, y being Element of Aut G holds b2 . (x,y) = x * y ) implies b1 = b2 )
assume that
A2: for x, y being Element of Aut G holds b1 . (x,y) = x * y and
A3: for x, y being Element of Aut G holds b2 . (x,y) = x * y ; ::_thesis: b1 = b2
 for x, y being Element of Aut G holds b1 . (x,y) = b2 . (x,y)
proof
let x, y be Element of Aut G; ::_thesis: b1 . (x,y) = b2 . (x,y)
thus b1 . (x,y) = x * y by A2
.= b2 . (x,y) by A3 ; ::_thesis: verum
end;
hence  b1 = b2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines AutComp AUTGROUP:def_2_:_
 for G being strict Group
for b2 being BinOp of (Aut G) holds
( b2 = AutComp G iff for x, y being Element of Aut G holds b2 . (x,y) = x * y );

definition
let G be strict Group;
func AutGroup G ->  strict Group equals :: AUTGROUP:def 3
 multMagma(# (Aut G),(AutComp G) #);
coherence
 multMagma(# (Aut G),(AutComp G) #) is strict Group
proof
set H = multMagma(# (Aut G),(AutComp G) #);
A1: ex e being Element of multMagma(# (Aut G),(AutComp G) #) st
for h being Element of multMagma(# (Aut G),(AutComp G) #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st
( h * g = e & g * h = e ) )
proof
reconsider e = id the carrier of G as Element of multMagma(# (Aut G),(AutComp G) #) by Th3;
take  e ; ::_thesis: for h being Element of multMagma(# (Aut G),(AutComp G) #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st
( h * g = e & g * h = e ) )
let h be Element of multMagma(# (Aut G),(AutComp G) #); ::_thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st
( h * g = e & g * h = e ) )
consider A being Element of Aut G such that
A2: A = h ;
h * e = A * (id the carrier of G) by A2, Def2
.= A by FUNCT_2:17 ;
hence  h * e = h by A2; ::_thesis: ( e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st
( h * g = e & g * h = e ) )
e * h = (id the carrier of G) * A by A2, Def2
.= A by FUNCT_2:17 ;
hence  e * h = h by A2; ::_thesis: ex g being Element of multMagma(# (Aut G),(AutComp G) #) st
( h * g = e & g * h = e )
reconsider g = A " as Element of multMagma(# (Aut G),(AutComp G) #) by Th6;
take  g ; ::_thesis: ( h * g = e & g * h = e )
reconsider A = A as Homomorphism of G,G by Def1;
A3: A is one-to-one by Def1;
 A is onto by Def1;
then A4: rng A = the carrier of G by FUNCT_2:def_3;
thus h * g = A * (A ") by A2, Def2
.= e by A3, A4, FUNCT_2:29 ; ::_thesis: g * h = e
thus g * h = (A ") * A by A2, Def2
.= e by A3, A4, FUNCT_2:29 ; ::_thesis: verum
end;
 for f, g, h being Element of multMagma(# (Aut G),(AutComp G) #) holds (f * g) * h = f * (g * h)
proof
let f, g, h be Element of multMagma(# (Aut G),(AutComp G) #); ::_thesis: (f * g) * h = f * (g * h)
reconsider A = f, B = g, C = h as Element of Aut G ;
A5: g * h = B * C by Def2;
 f * g = A * B by Def2;
hence (f * g) * h = (A * B) * C by Def2
.= A * (B * C) by RELAT_1:36
.= f * (g * h) by A5, Def2 ;
::_thesis: verum
end;
hence  multMagma(# (Aut G),(AutComp G) #) is strict Group by A1, GROUP_1:def_2, GROUP_1:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines AutGroup AUTGROUP:def_3_:_
 for G being strict Group holds AutGroup G = multMagma(# (Aut G),(AutComp G) #);

theorem :: AUTGROUP:8
for G being strict Group
for x, y being Element of (AutGroup G)
for f, g being Element of Aut G st x = f & y = g holds
x * y = f * g by Def2;

theorem Th9: :: AUTGROUP:9
for G being strict Group holds id the carrier of G = 1_ (AutGroup G)
proof
let G be strict Group; ::_thesis: id the carrier of G = 1_ (AutGroup G)
set f = the Element of (AutGroup G);
reconsider g = id the carrier of G as Element of (AutGroup G) by Th3;
consider g1 being Function of the carrier of G, the carrier of G such that
A1: g1 = g ;
 the Element of (AutGroup G) is Homomorphism of G,G by Def1;
then consider f1 being Function of the carrier of G, the carrier of G such that
A2: f1 = the Element of (AutGroup G) ;
 ( f1 = the Element of (AutGroup G) & g1 = g implies f1 * g1 = the Element of (AutGroup G) * g ) by Def2;
hence  id the carrier of G = 1_ (AutGroup G) by A1, A2, FUNCT_2:17, GROUP_1:7; ::_thesis: verum
end;

theorem Th10: :: AUTGROUP:10
for G being strict Group
for f being Element of Aut G
for g being Element of (AutGroup G) st f = g holds
f " = g "
proof
let G be strict Group; ::_thesis: for f being Element of Aut G
for g being Element of (AutGroup G) st f = g holds
f " = g "
let f be Element of Aut G; ::_thesis: for g being Element of (AutGroup G) st f = g holds
f " = g "
let g be Element of (AutGroup G); ::_thesis: ( f = g implies f " = g " )
consider g1 being Element of Aut G such that
A1: g1 = g " ;
assume  f = g ; ::_thesis: f " = g "
then  g1 * f = (g ") * g by A1, Def2;
then  g1 * f = 1_ (AutGroup G) by GROUP_1:def_5;
then A2: g1 * f = id the carrier of G by Th9;
 f is Homomorphism of G,G by Def1;
then A3: f is one-to-one by Def1;
rng f = dom f by Lm3
.= the carrier of G by Lm3 ;
hence  f " = g " by A1, A3, A2, FUNCT_2:30; ::_thesis: verum
end;

definition
let G be strict Group;
func InnAut G ->  FUNCTION_DOMAIN of the carrier of G, the carrier of G means :Def4: :: AUTGROUP:def 4
 for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in it iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a );
existence
 ex b1 being FUNCTION_DOMAIN of the carrier of G, the carrier of G st
for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in b1 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a )
proof
set I = id the carrier of G;
set X =  {  f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st
for x being Element of G holds f . x = x |^ a  }  ;
A1: ex a being Element of G st
for x being Element of G holds (id the carrier of G) . x = x |^ a
proof
take a = 1_ G; ::_thesis: for x being Element of G holds (id the carrier of G) . x = x |^ a
let x be Element of G; ::_thesis: (id the carrier of G) . x = x |^ a
A2: a " = 1_ G by GROUP_1:8;
thus (id the carrier of G) . x = x by FUNCT_1:18
.= x * a by GROUP_1:def_4
.= x |^ a by A2, GROUP_1:def_4 ; ::_thesis: verum
end;
 id the carrier of G is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
then A3: id the carrier of G in  {  f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st
for x being Element of G holds f . x = x |^ a  }  by A1;
  {  f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st
for x being Element of G holds f . x = x |^ a  }  is functional
proof
let h be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not h in  {  f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st
for x being Element of G holds f . x = x |^ a  }  or h is set )
assume  h in  {  f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st
for x being Element of G holds f . x = x |^ a  }  ; ::_thesis: h is set
then  ex f being Element of Funcs ( the carrier of G, the carrier of G) st
( f = h & ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) ;
hence  h is set ; ::_thesis: verum
end;
then reconsider X =  {  f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st
for x being Element of G holds f . x = x |^ a  }  as functional non empty set by A3;
 X is FUNCTION_DOMAIN of the carrier of G, the carrier of G
proof
let h be Element of X; :: according to FUNCT_2:def_12 ::_thesis: h is Element of bool [: the carrier of G, the carrier of G:]
 h in X ;
then  ex f being Element of Funcs ( the carrier of G, the carrier of G) st
( f = h & ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) ;
hence  h is Element of bool [: the carrier of G, the carrier of G:] ; ::_thesis: verum
end;
then reconsider X = X as FUNCTION_DOMAIN of the carrier of G, the carrier of G ;
take  X ; ::_thesis: for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in X iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a )
let f be Element of Funcs ( the carrier of G, the carrier of G); ::_thesis: ( f in X iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a )
hereby  ::_thesis: ( ex a being Element of G st
for x being Element of G holds f . x = x |^ a implies f in X )
assume  f in X ; ::_thesis: ex a being Element of G st
for x being Element of G holds f . x = x |^ a
then  ex f1 being Element of Funcs ( the carrier of G, the carrier of G) st
( f1 = f & ex a being Element of G st
for x being Element of G holds f1 . x = x |^ a ) ;
hence  ex a being Element of G st
for x being Element of G holds f . x = x |^ a ; ::_thesis: verum
end;
thus  ( ex a being Element of G st
for x being Element of G holds f . x = x |^ a implies f in X ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FUNCTION_DOMAIN of the carrier of G, the carrier of G st ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in b1 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) ) & ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in b2 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) ) holds
b1 = b2
proof
let F1, F2 be FUNCTION_DOMAIN of the carrier of G, the carrier of G; ::_thesis: ( ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in F1 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) ) & ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in F2 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) ) implies F1 = F2 )
assume that
A4: for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in F1 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) and
A5: for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in F2 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) ; ::_thesis: F1 = F2
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  q is Function of the carrier of G, the carrier of G by FUNCT_2:def_12;
then reconsider b1 = q as Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
 ex a being Element of G st
for x being Element of G holds b1 . x = x |^ a by A5, A7;
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 A8: q in F1 ; ::_thesis: q in F2
then  q is Function of the carrier of G, the carrier of G by FUNCT_2:def_12;
then reconsider b1 = q as Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
 ex a being Element of G st
for x being Element of G holds b1 . x = x |^ a by A4, A8;
hence  q in F2 by A5; ::_thesis: verum
end;
hence  F1 = F2 by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines InnAut AUTGROUP:def_4_:_
 for G being strict Group
for b2 being FUNCTION_DOMAIN of the carrier of G, the carrier of G holds
( b2 = InnAut G iff for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in b2 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) );

theorem :: AUTGROUP:11
for G being strict Group holds InnAut G c= Funcs ( the carrier of G, the carrier of G)
proof
let G be strict Group; ::_thesis: InnAut G c= Funcs ( the carrier of G, the carrier of G)
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in InnAut G or q in Funcs ( the carrier of G, the carrier of G) )
assume  q in InnAut G ; ::_thesis: q in Funcs ( the carrier of G, the carrier of G)
then  ex f being Element of InnAut G st f = q ;
hence  q in Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9; ::_thesis: verum
end;

theorem Th12: :: AUTGROUP:12
for G being strict Group
for f being Element of InnAut G holds f is Element of Aut G
proof
let G be strict Group; ::_thesis: for f being Element of InnAut G holds f is Element of Aut G
let f be Element of InnAut G; ::_thesis: f is Element of Aut G
A1: f is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
now__::_thesis:_for_x,_y_being_Element_of_G_holds_f_._(x_*_y)_=_(f_._x)_*_(f_._y)
let x, y be Element of G; ::_thesis: f . (x * y) = (f . x) * (f . y)
consider a being Element of G such that
A2: for x being Element of G holds f . x = x |^ a by A1, Def4;
thus f . (x * y) = (x * y) |^ a by A2
.= (((a ") * x) * y) * a by GROUP_1:def_3
.= ((a ") * x) * (y * a) by GROUP_1:def_3
.= (((a ") * x) * (1_ G)) * (y * a) by GROUP_1:def_4
.= (((a ") * x) * (a * (a "))) * (y * a) by GROUP_1:def_5
.= ((((a ") * x) * a) * (a ")) * (y * a) by GROUP_1:def_3
.= (((((a ") * x) * a) * (a ")) * y) * a by GROUP_1:def_3
.= ((((a ") * x) * a) * ((a ") * y)) * a by GROUP_1:def_3
.= (x |^ a) * (y |^ a) by GROUP_1:def_3
.= (f . x) * (y |^ a) by A2
.= (f . x) * (f . y) by A2 ; ::_thesis: verum
end;
then reconsider f = f as Homomorphism of G,G by GROUP_6:def_6;
A3: f is one-to-one
proof
let q be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not q in dom f or not b1 in dom f or not f . q = f . b1 or q = b1 )
let q1 be set ; ::_thesis: ( not q in dom f or not q1 in dom f or not f . q = f . q1 or q = q1 )
assume that
A4: ( q in dom f & q1 in dom f ) and
A5: f . q = f . q1 ; ::_thesis: q = q1
consider x, y being Element of G such that
A6: ( x = q & y = q1 ) by A4;
consider a being Element of G such that
A7: for x being Element of G holds f . x = x |^ a by A1, Def4;
 f . x = y |^ a by A7, A5, A6;
then  x |^ a = y |^ a by A7;
then  a * ((a ") * (x * a)) = a * (((a ") * y) * a) by GROUP_1:def_3;
then  (a * (a ")) * (x * a) = a * (((a ") * y) * a) by GROUP_1:def_3;
then  (a * (a ")) * (x * a) = a * ((a ") * (y * a)) by GROUP_1:def_3;
then  (a * (a ")) * (x * a) = (a * (a ")) * (y * a) by GROUP_1:def_3;
then  (1_ G) * (x * a) = (a * (a ")) * (y * a) by GROUP_1:def_5;
then  (1_ G) * (x * a) = (1_ G) * (y * a) by GROUP_1:def_5;
then  x * a = (1_ G) * (y * a) by GROUP_1:def_4;
then  (x * a) * (a ") = (y * a) * (a ") by GROUP_1:def_4;
then  x * (a * (a ")) = (y * a) * (a ") by GROUP_1:def_3;
then  x * (a * (a ")) = y * (a * (a ")) by GROUP_1:def_3;
then  x * (1_ G) = y * (a * (a ")) by GROUP_1:def_5;
then  x * (1_ G) = y * (1_ G) by GROUP_1:def_5;
then  x = y * (1_ G) by GROUP_1:def_4;
hence  q = q1 by A6, GROUP_1:def_4; ::_thesis: verum
end;
 for q being set st q in the carrier of G holds
ex q1 being set st
( q1 in dom f & q = f . q1 )
proof
let q be set ; ::_thesis: ( q in the carrier of G implies ex q1 being set st
( q1 in dom f & q = f . q1 ) )
assume  q in the carrier of G ; ::_thesis: ex q1 being set st
( q1 in dom f & q = f . q1 )
then consider y being Element of G such that
A8: y = q ;
consider a being Element of G such that
A9: for x being Element of G holds f . x = x |^ a by A1, Def4;
take q1 = (a * y) * (a "); ::_thesis: ( q1 in dom f & q = f . q1 )
 ex f1 being Function st
( f = f1 & dom f1 = the carrier of G & rng f1 c= the carrier of G ) by A1, FUNCT_2:def_2;
hence  q1 in dom f ; ::_thesis: q = f . q1
y = (1_ G) * y by GROUP_1:def_4
.= ((1_ G) * y) * (1_ G) by GROUP_1:def_4
.= (((a ") * a) * y) * (1_ G) by GROUP_1:def_5
.= (((a ") * a) * y) * ((a ") * a) by GROUP_1:def_5
.= ((((a ") * a) * y) * (a ")) * a by GROUP_1:def_3
.= (((a ") * a) * (y * (a "))) * a by GROUP_1:def_3
.= ((a ") * (a * (y * (a ")))) * a by GROUP_1:def_3
.= q1 |^ a by GROUP_1:def_3
.= f . q1 by A9 ;
hence  q = f . q1 by A8; ::_thesis: verum
end;
then  the carrier of G c= rng f by FUNCT_1:9;
then  rng f = the carrier of G by XBOOLE_0:def_10;
then  f is onto by FUNCT_2:def_3;
hence  f is Element of Aut G by A3, Def1; ::_thesis: verum
end;

theorem Th13: :: AUTGROUP:13
for G being strict Group holds InnAut G c= Aut G
proof
let G be strict Group; ::_thesis: InnAut G c= Aut G
now__::_thesis:_for_q_being_set_st_q_in_InnAut_G_holds_
q_in_Aut_G
let q be set ; ::_thesis: ( q in InnAut G implies q in Aut G )
assume  q in InnAut G ; ::_thesis: q in Aut G
then consider f being Element of InnAut G such that
A1: f = q ;
 f is Element of Aut G by Th12;
hence  q in Aut G by A1; ::_thesis: verum
end;
hence  InnAut G c= Aut G by TARSKI:def_3; ::_thesis: verum
end;

theorem Th14: :: AUTGROUP:14
for G being strict Group
for f, g being Element of InnAut G holds (AutComp G) . (f,g) = f * g
proof
let G be strict Group; ::_thesis: for f, g being Element of InnAut G holds (AutComp G) . (f,g) = f * g
let f, g be Element of InnAut G; ::_thesis: (AutComp G) . (f,g) = f * g
 ( f is Element of Aut G & g is Element of Aut G ) by Th12;
hence  (AutComp G) . (f,g) = f * g by Def2; ::_thesis: verum
end;

theorem Th15: :: AUTGROUP:15
for G being strict Group holds id the carrier of G is Element of InnAut G
proof
let G be strict Group; ::_thesis: id the carrier of G is Element of InnAut G
set I = id the carrier of G;
A1: ex a being Element of G st
for x being Element of G holds (id the carrier of G) . x = x |^ a
proof
take a = 1_ G; ::_thesis: for x being Element of G holds (id the carrier of G) . x = x |^ a
let x be Element of G; ::_thesis: (id the carrier of G) . x = x |^ a
A2: a " = 1_ G by GROUP_1:8;
thus (id the carrier of G) . x = x by FUNCT_1:18
.= x * a by GROUP_1:def_4
.= x |^ a by A2, GROUP_1:def_4 ; ::_thesis: verum
end;
 id the carrier of G is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
hence  id the carrier of G is Element of InnAut G by A1, Def4; ::_thesis: verum
end;

theorem Th16: :: AUTGROUP:16
for G being strict Group
for f being Element of InnAut G holds f " is Element of InnAut G
proof
let G be strict Group; ::_thesis: for f being Element of InnAut G holds f " is Element of InnAut G
let f be Element of InnAut G; ::_thesis: f " is Element of InnAut G
reconsider f1 = f as Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
 f1 = f ;
then consider f1 being Element of Funcs ( the carrier of G, the carrier of G) such that
A1: f1 = f ;
A2: ex a being Element of G st
for x being Element of G holds (f ") . x = x |^ a
proof
consider b being Element of G such that
A3: for y being Element of G holds f1 . y = y |^ b by A1, Def4;
take a = b " ; ::_thesis: for x being Element of G holds (f ") . x = x |^ a
let x be Element of G; ::_thesis: (f ") . x = x |^ a
A4: f1 is Element of Aut G by A1, Th12;
then reconsider f1 = f1 as Homomorphism of G,G by Def1;
A5: f1 is bijective by A4, Th4;
then consider y1 being Element of G such that
A6: x = f1 . y1 by GROUP_6:58;
(f1 ") . x = y1 by A5, A6, FUNCT_2:26
.= (1_ G) * y1 by GROUP_1:def_4
.= ((1_ G) * y1) * (1_ G) by GROUP_1:def_4
.= ((b * (b ")) * y1) * (1_ G) by GROUP_1:def_5
.= ((b * (b ")) * y1) * (b * (b ")) by GROUP_1:def_5
.= (((b * (b ")) * y1) * b) * (b ") by GROUP_1:def_3
.= ((b * (b ")) * (y1 * b)) * (b ") by GROUP_1:def_3
.= (b * ((b ") * (y1 * b))) * (b ") by GROUP_1:def_3
.= (b * (y1 |^ b)) * (b ") by GROUP_1:def_3
.= (b * x) * (b ") by A3, A6
.= ((a ") * x) * a ;
hence  (f ") . x = x |^ a by A1; ::_thesis: verum
end;
A7: f is Element of Aut G by Th12;
then reconsider f2 = f as Homomorphism of G,G by Def1;
 f2 = f ;
then consider f2 being Homomorphism of G,G such that
A8: f2 = f ;
 f2 is onto by A7, A8, Def1;
then A9: rng f2 = the carrier of G by FUNCT_2:def_3;
 f2 is one-to-one by A7, A8, Def1;
then  f " is Function of the carrier of G, the carrier of G by A8, A9, FUNCT_2:25;
then  f " is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
hence  f " is Element of InnAut G by A2, Def4; ::_thesis: verum
end;

theorem Th17: :: AUTGROUP:17
for G being strict Group
for f, g being Element of InnAut G holds f * g is Element of InnAut G
proof
let G be strict Group; ::_thesis: for f, g being Element of InnAut G holds f * g is Element of InnAut G
let f, g be Element of InnAut G; ::_thesis: f * g is Element of InnAut G
A1: g is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
A2: f is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
A3: ex a being Element of G st
for x being Element of G holds (f * g) . x = x |^ a
proof
consider c being Element of G such that
A4: for x2 being Element of G holds g . x2 = x2 |^ c by A1, Def4;
consider b being Element of G such that
A5: for x1 being Element of G holds f . x1 = x1 |^ b by A2, Def4;
take a = c * b; ::_thesis: for x being Element of G holds (f * g) . x = x |^ a
let x be Element of G; ::_thesis: (f * g) . x = x |^ a
(f * g) . x = f . (g . x) by FUNCT_2:15
.= f . (x |^ c) by A4
.= (((c ") * x) * c) |^ b by A5
.= (b ") * ((((c ") * x) * c) * b) by GROUP_1:def_3
.= (b ") * (((c ") * (x * c)) * b) by GROUP_1:def_3
.= (b ") * ((c ") * ((x * c) * b)) by GROUP_1:def_3
.= ((b ") * (c ")) * ((x * c) * b) by GROUP_1:def_3
.= ((b ") * (c ")) * (x * (c * b)) by GROUP_1:def_3
.= (((b ") * (c ")) * x) * (c * b) by GROUP_1:def_3
.= x |^ a by GROUP_1:17 ;
hence  (f * g) . x = x |^ a ; ::_thesis: verum
end;
 f * g is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
hence  f * g is Element of InnAut G by A3, Def4; ::_thesis: verum
end;

definition
let G be strict Group;
func InnAutGroup G ->  strict normal Subgroup of AutGroup G means :Def5: :: AUTGROUP:def 5
 the carrier of it = InnAut G;
existence
 ex b1 being strict normal Subgroup of AutGroup G st the carrier of b1 = InnAut G
proof
reconsider K1 = Aut G as set ;
reconsider K2 = InnAut G as Subset of K1 by Th13;
 for q being set st q in [:K2,K2:] holds
(AutComp G) . q in K2
proof
let q be set ; ::_thesis: ( q in [:K2,K2:] implies (AutComp G) . q in K2 )
assume  q in [:K2,K2:] ; ::_thesis: (AutComp G) . q in K2
then consider x, y being set  such that
A1: ( x in K2 & y in K2 ) and
A2: q = [x,y] by ZFMISC_1:def_2;
reconsider x = x, y = y as Element of InnAut G by A1;
A3: x * y is Element of InnAut G by Th17;
(AutComp G) . q = (AutComp G) . (x,y) by A2
.= x * y by Th14 ;
hence  (AutComp G) . q in K2 by A3; ::_thesis: verum
end;
then  AutComp G is Presv of K1,K2 by REALSET1:def_4;
then reconsider op = (AutComp G) || (InnAut G) as BinOp of (InnAut G) by REALSET1:6;
set IG = multMagma(# (InnAut G),op #);
A4: now__::_thesis:_for_x,_y_being_Element_of_multMagma(#_(InnAut_G),op_#)
for_f,_g_being_Element_of_InnAut_G_st_x_=_f_&_y_=_g_holds_
x_*_y_=_f_*_g
let x, y be Element of multMagma(# (InnAut G),op #); ::_thesis: for f, g being Element of InnAut G st x = f & y = g holds
x * y = f * g
let f, g be Element of InnAut G; ::_thesis: ( x = f & y = g implies x * y = f * g )
A5: [f,g] in [:(InnAut G),(InnAut G):] by ZFMISC_1:def_2;
assume  ( x = f & y = g ) ; ::_thesis: x * y = f * g
hence x * y = (AutComp G) . (f,g) by A5, FUNCT_1:49
.= f * g by Th14 ;
::_thesis: verum
end;
A6: for f, g, h being Element of multMagma(# (InnAut G),op #) holds (f * g) * h = f * (g * h)
proof
let f, g, h be Element of multMagma(# (InnAut G),op #); ::_thesis: (f * g) * h = f * (g * h)
reconsider A = f, B = g, C = h as Element of InnAut G ;
A7: g * h = B * C by A4;
 f * g = A * B by A4;
hence (f * g) * h = (A * B) * C by A4
.= A * (B * C) by RELAT_1:36
.= f * (g * h) by A4, A7 ;
::_thesis: verum
end;
 ex e being Element of multMagma(# (InnAut G),op #) st
for h being Element of multMagma(# (InnAut G),op #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (InnAut G),op #) st
( h * g = e & g * h = e ) )
proof
reconsider e = id the carrier of G as Element of multMagma(# (InnAut G),op #) by Th15;
take  e ; ::_thesis: for h being Element of multMagma(# (InnAut G),op #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (InnAut G),op #) st
( h * g = e & g * h = e ) )
let h be Element of multMagma(# (InnAut G),op #); ::_thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (InnAut G),op #) st
( h * g = e & g * h = e ) )
consider A being Element of InnAut G such that
A8: A = h ;
h * e = A * (id the carrier of G) by A4, A8
.= A by FUNCT_2:17 ;
hence  h * e = h by A8; ::_thesis: ( e * h = h & ex g being Element of multMagma(# (InnAut G),op #) st
( h * g = e & g * h = e ) )
e * h = (id the carrier of G) * A by A4, A8
.= A by FUNCT_2:17 ;
hence  e * h = h by A8; ::_thesis: ex g being Element of multMagma(# (InnAut G),op #) st
( h * g = e & g * h = e )
reconsider g = A " as Element of multMagma(# (InnAut G),op #) by Th16;
take  g ; ::_thesis: ( h * g = e & g * h = e )
reconsider A = A as Element of Aut G by Th12;
reconsider A = A as Homomorphism of G,G by Def1;
A9: A is one-to-one by Def1;
 A is onto by Def1;
then A10: rng A = the carrier of G by FUNCT_2:def_3;
thus h * g = A * (A ") by A4, A8
.= e by A9, A10, FUNCT_2:29 ; ::_thesis: g * h = e
thus g * h = (A ") * A by A4, A8
.= e by A9, A10, FUNCT_2:29 ; ::_thesis: verum
end;
then reconsider IG = multMagma(# (InnAut G),op #) as Group by A6, GROUP_1:def_2, GROUP_1:def_3;
 the carrier of IG c= the carrier of (AutGroup G) by Th13;
then reconsider IG = IG as strict Subgroup of AutGroup G by GROUP_2:def_5;
 for f, k being Element of (AutGroup G) st k is Element of IG holds
k |^ f in IG
proof
let f, k be Element of (AutGroup G); ::_thesis: ( k is Element of IG implies k |^ f in IG )
consider f1 being Element of Aut G such that
A11: f1 = f ;
assume  k is Element of IG ; ::_thesis: k |^ f in IG
then consider g being Element of InnAut G such that
A12: g = k ;
reconsider D = g as Element of Aut G by Th12;
 g is Element of Aut G by Th12;
then consider g1 being Element of Aut G such that
A13: g1 = g ;
 g1 is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
then consider a being Element of G such that
A14: for x being Element of G holds g1 . x = x |^ a by A13, Def4;
 ((f1 ") * g1) * f1 is Element of InnAut G
proof
 f1 is Homomorphism of G,G by Def1;
then A15: f1 is one-to-one by Def1;
A16: rng f1 = dom f1 by Lm3
.= the carrier of G by Lm3 ;
then  f1 " is Function of the carrier of G, the carrier of G by A15, FUNCT_2:25;
then  (f1 ") * g1 is Function of the carrier of G, the carrier of G by FUNCT_2:13;
then  ((f1 ") * g1) * f1 is Function of the carrier of G, the carrier of G by FUNCT_2:13;
then A17: ((f1 ") * g1) * f1 is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
 f1 " is Element of Aut G by Th6;
then  f1 " is Homomorphism of G,G by Def1;
then consider A being Homomorphism of G,G such that
A18: A = f1 " ;
A19: A * f1 = id the carrier of G by A15, A16, A18, FUNCT_2:29;
now__::_thesis:_for_y_being_Element_of_G_holds_(((f1_")_*_g1)_*_f1)_._y_=_y_|^_(A_._a)
let y be Element of G; ::_thesis: (((f1 ") * g1) * f1) . y = y |^ (A . a)
thus (((f1 ") * g1) * f1) . y = ((f1 ") * (g1 * f1)) . y by RELAT_1:36
.= (f1 ") . ((g1 * f1) . y) by FUNCT_2:15
.= (f1 ") . (g1 . (f1 . y)) by FUNCT_2:15
.= (f1 ") . ((f1 . y) |^ a) by A14
.= (A . ((a ") * (f1 . y))) * (A . a) by A18, GROUP_6:def_6
.= ((A . (a ")) * (A . (f1 . y))) * (A . a) by GROUP_6:def_6
.= ((A . (a ")) * ((A * f1) . y)) * (A . a) by FUNCT_2:15
.= ((A . (a ")) * y) * (A . a) by A19, FUNCT_1:18
.= y |^ (A . a) by GROUP_6:32 ; ::_thesis: verum
end;
hence  ((f1 ") * g1) * f1 is Element of InnAut G by A17, Def4; ::_thesis: verum
end;
then A20: ((f1 ") * g) * f1 in InnAut G by A13;
reconsider C = f1 " as Element of Aut G by Th6;
consider q being set  such that
A21: q = ((f ") * k) * f ;
 f1 " = f " by A11, Th10;
then  C * D = (f ") * k by A12, Def2;
then  q in carr IG by A11, A20, A21, Def2;
hence  k |^ f in IG by A21, STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider IG = IG as strict normal Subgroup of AutGroup G by Lm1;
take  IG ; ::_thesis: the carrier of IG = InnAut G
thus  the carrier of IG = InnAut G ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict normal Subgroup of AutGroup G st the carrier of b1 = InnAut G & the carrier of b2 = InnAut G holds
b1 = b2 by GROUP_2:59;
end;

:: deftheorem Def5 defines InnAutGroup AUTGROUP:def_5_:_
 for G being strict Group
for b2 being strict normal Subgroup of AutGroup G holds
( b2 = InnAutGroup G iff the carrier of b2 = InnAut G );

theorem Th18: :: AUTGROUP:18
for G being strict Group
for x, y being Element of (InnAutGroup G)
for f, g being Element of InnAut G st x = f & y = g holds
x * y = f * g
proof
let G be strict Group; ::_thesis: for x, y being Element of (InnAutGroup G)
for f, g being Element of InnAut G st x = f & y = g holds
x * y = f * g
let x, y be Element of (InnAutGroup G); ::_thesis: for f, g being Element of InnAut G st x = f & y = g holds
x * y = f * g
let f, g be Element of InnAut G; ::_thesis: ( x = f & y = g implies x * y = f * g )
 ( x is Element of (AutGroup G) & y is Element of (AutGroup G) ) by GROUP_2:42;
then consider x1, y1 being Element of (AutGroup G) such that
A1: ( x1 = x & y1 = y ) ;
 ( f is Element of Aut G & g is Element of Aut G ) by Th12;
then consider f1, g1 being Element of Aut G such that
A2: ( f1 = f & g1 = g ) ;
assume  ( x = f & y = g ) ; ::_thesis: x * y = f * g
then  x1 * y1 = f1 * g1 by A2, A1, Def2;
hence  x * y = f * g by A2, A1, GROUP_2:43; ::_thesis: verum
end;

theorem Th19: :: AUTGROUP:19
for G being strict Group holds id the carrier of G = 1_ (InnAutGroup G)
proof
let G be strict Group; ::_thesis: id the carrier of G = 1_ (InnAutGroup G)
 id the carrier of G = 1_ (AutGroup G) by Th9;
hence  id the carrier of G = 1_ (InnAutGroup G) by GROUP_2:44; ::_thesis: verum
end;

theorem :: AUTGROUP:20
for G being strict Group
for f being Element of InnAut G
for g being Element of (InnAutGroup G) st f = g holds
f " = g "
proof
let G be strict Group; ::_thesis: for f being Element of InnAut G
for g being Element of (InnAutGroup G) st f = g holds
f " = g "
let f be Element of InnAut G; ::_thesis: for g being Element of (InnAutGroup G) st f = g holds
f " = g "
let g be Element of (InnAutGroup G); ::_thesis: ( f = g implies f " = g " )
 g is Element of (AutGroup G) by GROUP_2:42;
then consider g1 being Element of (AutGroup G) such that
A1: g1 = g ;
 f is Element of Aut G by Th12;
then consider f1 being Element of Aut G such that
A2: f1 = f ;
assume  f = g ; ::_thesis: f " = g "
then  f1 " = g1 " by A2, A1, Th10;
hence  f " = g " by A2, A1, GROUP_2:48; ::_thesis: verum
end;

definition
let G be strict Group;
let b be Element of G;
func Conjugate b ->  Element of InnAut G means :Def6: :: AUTGROUP:def 6
 for a being Element of G holds it . a = a |^ b;
existence
 ex b1 being Element of InnAut G st
for a being Element of G holds b1 . a = a |^ b
proof
deffunc H1( Element of G) ->  Element of the carrier of G = $1 |^ b;
consider g being Function of the carrier of G, the carrier of G such that
A1: for a being Element of G holds g . a = H1(a) from FUNCT_2:sch_4();
 g is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
then reconsider g = g as Element of InnAut G by A1, Def4;
take  g ; ::_thesis: for a being Element of G holds g . a = a |^ b
let a be Element of G; ::_thesis: g . a = a |^ b
thus  g . a = a |^ b by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of InnAut G st ( for a being Element of G holds b1 . a = a |^ b ) & ( for a being Element of G holds b2 . a = a |^ b ) holds
b1 = b2
proof
let f1, f2 be Element of InnAut G; ::_thesis: ( ( for a being Element of G holds f1 . a = a |^ b ) & ( for a being Element of G holds f2 . a = a |^ b ) implies f1 = f2 )
assume that
A2: for a being Element of G holds f1 . a = a |^ b and
A3: for a being Element of G holds f2 . a = a |^ b ; ::_thesis: f1 = f2
 for a being Element of G holds f1 . a = f2 . a
proof
let a be Element of G; ::_thesis: f1 . a = f2 . a
thus f1 . a = a |^ b by A2
.= f2 . a by A3 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Conjugate AUTGROUP:def_6_:_
 for G being strict Group
for b being Element of G
for b3 being Element of InnAut G holds
( b3 = Conjugate b iff for a being Element of G holds b3 . a = a |^ b );

theorem Th21: :: AUTGROUP:21
for G being strict Group
for a, b being Element of G holds Conjugate (a * b) = (Conjugate b) * (Conjugate a)
proof
let G be strict Group; ::_thesis: for a, b being Element of G holds Conjugate (a * b) = (Conjugate b) * (Conjugate a)
let a, b be Element of G; ::_thesis: Conjugate (a * b) = (Conjugate b) * (Conjugate a)
set f1 = Conjugate (a * b);
set f2 = (Conjugate b) * (Conjugate a);
A1: for c being Element of G holds (Conjugate (a * b)) . c = (c |^ a) |^ b
proof
let c be Element of G; ::_thesis: (Conjugate (a * b)) . c = (c |^ a) |^ b
 c |^ (a * b) = (c |^ a) |^ b by GROUP_3:24;
hence  (Conjugate (a * b)) . c = (c |^ a) |^ b by Def6; ::_thesis: verum
end;
A2: for c being Element of G holds (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a)
proof
let c be Element of G; ::_thesis: (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a)
 (c |^ a) |^ b = (Conjugate b) . (c |^ a) by Def6;
hence  (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a) by A1; ::_thesis: verum
end;
A3: for c being Element of G holds (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c)
proof
let c be Element of G; ::_thesis: (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c)
 (Conjugate b) . (c |^ a) = (Conjugate b) . ((Conjugate a) . c) by Def6;
hence  (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c) by A2; ::_thesis: verum
end;
 for c being Element of G holds (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c
proof
let c be Element of G; ::_thesis: (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c
 (Conjugate b) . ((Conjugate a) . c) = ((Conjugate b) * (Conjugate a)) . c by FUNCT_2:15;
hence  (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c by A3; ::_thesis: verum
end;
hence  Conjugate (a * b) = (Conjugate b) * (Conjugate a) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th22: :: AUTGROUP:22
for G being strict Group holds Conjugate (1_ G) = id the carrier of G
proof
let G be strict Group; ::_thesis: Conjugate (1_ G) = id the carrier of G
 for a being Element of G holds (Conjugate (1_ G)) . a = a
proof
let a be Element of G; ::_thesis: (Conjugate (1_ G)) . a = a
 a |^ (1_ G) = a by GROUP_3:19;
hence  (Conjugate (1_ G)) . a = a by Def6; ::_thesis: verum
end;
then A1: for q being set st q in the carrier of G holds
(Conjugate (1_ G)) . q = q ;
 Conjugate (1_ G) is Element of Aut G by Th12;
then  dom (Conjugate (1_ G)) = the carrier of G by Lm3;
hence  Conjugate (1_ G) = id the carrier of G by A1, FUNCT_1:17; ::_thesis: verum
end;

theorem Th23: :: AUTGROUP:23
for G being strict Group
for a being Element of G holds (Conjugate (1_ G)) . a = a
proof
let G be strict Group; ::_thesis: for a being Element of G holds (Conjugate (1_ G)) . a = a
let a be Element of G; ::_thesis: (Conjugate (1_ G)) . a = a
thus (Conjugate (1_ G)) . a = a |^ (1_ G) by Def6
.= a by GROUP_3:19 ; ::_thesis: verum
end;

theorem :: AUTGROUP:24
for G being strict Group
for a being Element of G holds (Conjugate a) * (Conjugate (a ")) = Conjugate (1_ G)
proof
let G be strict Group; ::_thesis: for a being Element of G holds (Conjugate a) * (Conjugate (a ")) = Conjugate (1_ G)
let a be Element of G; ::_thesis: (Conjugate a) * (Conjugate (a ")) = Conjugate (1_ G)
set f1 = (Conjugate a) * (Conjugate (a "));
set f2 = Conjugate (1_ G);
A1: for b being Element of G holds ((Conjugate a) * (Conjugate (a "))) . b = b
proof
let b be Element of G; ::_thesis: ((Conjugate a) * (Conjugate (a "))) . b = b
(Conjugate a) . ((Conjugate (a ")) . b) = (Conjugate a) . (b |^ (a ")) by Def6
.= (b |^ (a ")) |^ a by Def6
.= b by GROUP_3:25 ;
hence  ((Conjugate a) * (Conjugate (a "))) . b = b by FUNCT_2:15; ::_thesis: verum
end;
 for b being Element of G holds ((Conjugate a) * (Conjugate (a "))) . b = (Conjugate (1_ G)) . b
proof
let b be Element of G; ::_thesis: ((Conjugate a) * (Conjugate (a "))) . b = (Conjugate (1_ G)) . b
thus ((Conjugate a) * (Conjugate (a "))) . b = b by A1
.= (Conjugate (1_ G)) . b by Th23 ; ::_thesis: verum
end;
hence  (Conjugate a) * (Conjugate (a ")) = Conjugate (1_ G) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th25: :: AUTGROUP:25
for G being strict Group
for a being Element of G holds (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G)
proof
let G be strict Group; ::_thesis: for a being Element of G holds (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G)
let a be Element of G; ::_thesis: (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G)
set f1 = (Conjugate (a ")) * (Conjugate a);
set f2 = Conjugate (1_ G);
A1: for b being Element of G holds ((Conjugate (a ")) * (Conjugate a)) . b = b
proof
let b be Element of G; ::_thesis: ((Conjugate (a ")) * (Conjugate a)) . b = b
(Conjugate (a ")) . ((Conjugate a) . b) = (Conjugate (a ")) . (b |^ a) by Def6
.= (b |^ a) |^ (a ") by Def6
.= b by GROUP_3:25 ;
hence  ((Conjugate (a ")) * (Conjugate a)) . b = b by FUNCT_2:15; ::_thesis: verum
end;
 for b being Element of G holds ((Conjugate (a ")) * (Conjugate a)) . b = (Conjugate (1_ G)) . b
proof
let b be Element of G; ::_thesis: ((Conjugate (a ")) * (Conjugate a)) . b = (Conjugate (1_ G)) . b
thus ((Conjugate (a ")) * (Conjugate a)) . b = b by A1
.= (Conjugate (1_ G)) . b by Th23 ; ::_thesis: verum
end;
hence  (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: AUTGROUP:26
for G being strict Group
for a being Element of G holds Conjugate (a ") = (Conjugate a) "
proof
let G be strict Group; ::_thesis: for a being Element of G holds Conjugate (a ") = (Conjugate a) "
let a be Element of G; ::_thesis: Conjugate (a ") = (Conjugate a) "
set f = Conjugate a;
set g = Conjugate (a ");
A1: (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G) by Th25
.= id the carrier of G by Th22 ;
A2: Conjugate a is Element of Aut G by Th12;
then  Conjugate a is Homomorphism of G,G by Def1;
then A3: Conjugate a is one-to-one by A2, Def1;
rng (Conjugate a) = dom (Conjugate a) by A2, Lm3
.= the carrier of G by A2, Lm3 ;
hence  Conjugate (a ") = (Conjugate a) " by A1, A3, FUNCT_2:30; ::_thesis: verum
end;

theorem :: AUTGROUP:27
for G being strict Group
for a being Element of G holds
( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a )
proof
let G be strict Group; ::_thesis: for a being Element of G holds
( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a )
let a be Element of G; ::_thesis: ( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a )
 Conjugate (1_ G) = id the carrier of G by Th22;
hence  ( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a ) by FUNCT_2:17; ::_thesis: verum
end;

theorem :: AUTGROUP:28
for G being strict Group
for f being Element of InnAut G holds
( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f )
proof
let G be strict Group; ::_thesis: for f being Element of InnAut G holds
( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f )
let f be Element of InnAut G; ::_thesis: ( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f )
 Conjugate (1_ G) = id the carrier of G by Th22;
hence  ( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f ) by FUNCT_2:17; ::_thesis: verum
end;

theorem :: AUTGROUP:29
for G being strict Group holds InnAutGroup G,G ./. (center G) are_isomorphic
proof
let G be strict Group; ::_thesis: InnAutGroup G,G ./. (center G) are_isomorphic
deffunc H1( Element of G) ->  Element of InnAut G = Conjugate ($1 ");
consider f being Function of the carrier of G,(InnAut G) such that
A1: for a being Element of G holds f . a = H1(a) from FUNCT_2:sch_4();
reconsider f = f as Function of the carrier of G, the carrier of (InnAutGroup G) by Def5;
now__::_thesis:_for_a,_b_being_Element_of_G_holds_f_._(a_*_b)_=_(f_._a)_*_(f_._b)
let a, b be Element of G; ::_thesis: f . (a * b) = (f . a) * (f . b)
A2: f . (a * b) = Conjugate ((a * b) ") by A1
.= Conjugate ((b ") * (a ")) by GROUP_1:17
.= (Conjugate (a ")) * (Conjugate (b ")) by Th21 ;
now__::_thesis:_for_A,_B_being_Element_of_(InnAutGroup_G)_st_A_=_f_._a_&_B_=_f_._b_holds_
f_._(a_*_b)_=_(f_._a)_*_(f_._b)
let A, B be Element of (InnAutGroup G); ::_thesis: ( A = f . a & B = f . b implies f . (a * b) = (f . a) * (f . b) )
assume A3: ( A = f . a & B = f . b ) ; ::_thesis: f . (a * b) = (f . a) * (f . b)
then  ( A = Conjugate (a ") & B = Conjugate (b ") ) by A1;
hence  f . (a * b) = (f . a) * (f . b) by A2, A3, Th18; ::_thesis: verum
end;
hence  f . (a * b) = (f . a) * (f . b) ; ::_thesis: verum
end;
then reconsider f1 = f as Homomorphism of G,(InnAutGroup G) by GROUP_6:def_6;
A4: Ker f1 = center G
proof
set C =  {  a where a is Element of G : for b being Element of G holds a * b = b * a  }  ;
set KER = the carrier of (Ker f1);
A5: the carrier of (Ker f1) =  {  a where a is Element of G : f1 . a = 1_ (InnAutGroup G)  }  by GROUP_6:def_9;
A6: the carrier of (Ker f1) c=  {  a where a is Element of G : for b being Element of G holds a * b = b * a  }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in the carrier of (Ker f1) or q in  {  a where a is Element of G : for b being Element of G holds a * b = b * a  }  )
assume A7: q in the carrier of (Ker f1) ; ::_thesis: q in  {  a where a is Element of G : for b being Element of G holds a * b = b * a  }
 1_ (InnAutGroup G) = id the carrier of G by Th19;
then consider x being Element of G such that
A8: q = x and
A9: f1 . x = id the carrier of G by A5, A7;
A10: for b being Element of G holds (Conjugate (x ")) . b = b
proof
let b be Element of G; ::_thesis: (Conjugate (x ")) . b = b
 (id the carrier of G) . b = b by FUNCT_1:18;
hence  (Conjugate (x ")) . b = b by A1, A9; ::_thesis: verum
end;
A11: for b being Element of G holds b |^ (x ") = b
proof
let b be Element of G; ::_thesis: b |^ (x ") = b
 (Conjugate (x ")) . b = b |^ (x ") by Def6;
hence  b |^ (x ") = b by A10; ::_thesis: verum
end;
 for b being Element of G holds x * b = b * x
proof
let b be Element of G; ::_thesis: x * b = b * x
 b |^ (x ") = (x * b) * (x ") ;
then  ((x * b) * (x ")) * x = b * x by A11;
then  (x * b) * ((x ") * x) = b * x by GROUP_1:def_3;
then  (x * b) * (1_ G) = b * x by GROUP_1:def_5;
hence  x * b = b * x by GROUP_1:def_4; ::_thesis: verum
end;
hence  q in  {  a where a is Element of G : for b being Element of G holds a * b = b * a  }  by A8; ::_thesis: verum
end;
  {  a where a is Element of G : for b being Element of G holds a * b = b * a  }  c= the carrier of (Ker f1)
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  a where a is Element of G : for b being Element of G holds a * b = b * a  }  or q in the carrier of (Ker f1) )
assume  q in  {  a where a is Element of G : for b being Element of G holds a * b = b * a  }  ; ::_thesis: q in the carrier of (Ker f1)
then consider x being Element of G such that
A12: x = q and
A13: for b being Element of G holds x * b = b * x ;
consider g being Function of the carrier of G, the carrier of G such that
A14: g = Conjugate (x ") ;
A15: for b being Element of G holds b = (Conjugate (x ")) . b
proof
let b be Element of G; ::_thesis: b = (Conjugate (x ")) . b
 (x * b) * (x ") = (b * x) * (x ") by A13;
then  (x * b) * (x ") = b * (x * (x ")) by GROUP_1:def_3;
then  (x * b) * (x ") = b * (1_ G) by GROUP_1:def_5;
then  b = b |^ (x ") by GROUP_1:def_4;
hence  b = (Conjugate (x ")) . b by Def6; ::_thesis: verum
end;
 for b being Element of G holds (id the carrier of G) . b = g . b
proof
let b be Element of G; ::_thesis: (id the carrier of G) . b = g . b
 b = g . b by A15, A14;
hence  (id the carrier of G) . b = g . b by FUNCT_1:18; ::_thesis: verum
end;
then  g = id the carrier of G by FUNCT_2:63;
then  Conjugate (x ") = 1_ (InnAutGroup G) by A14, Th19;
then  f1 . x = 1_ (InnAutGroup G) by A1;
hence  q in the carrier of (Ker f1) by A5, A12; ::_thesis: verum
end;
then  the carrier of (Ker f1) =  {  a where a is Element of G : for b being Element of G holds a * b = b * a  }  by A6, XBOOLE_0:def_10;
hence  Ker f1 = center G by GROUP_5:def_10; ::_thesis: verum
end;
A16: the carrier of (InnAutGroup G) = InnAut G by Def5;
 for q being set st q in the carrier of (InnAutGroup G) holds
ex q1 being set st
( q1 in the carrier of G & q = f1 . q1 )
proof
let q be set ; ::_thesis: ( q in the carrier of (InnAutGroup G) implies ex q1 being set st
( q1 in the carrier of G & q = f1 . q1 ) )
assume A17: q in the carrier of (InnAutGroup G) ; ::_thesis: ex q1 being set st
( q1 in the carrier of G & q = f1 . q1 )
then A18: q is Element of InnAut G by Def5;
then consider y1 being Function of the carrier of G, the carrier of G such that
A19: y1 = q ;
 y1 is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
then consider b being Element of G such that
A20: for a being Element of G holds y1 . a = a |^ b by A16, A17, A19, Def4;
take q1 = b " ; ::_thesis: ( q1 in the carrier of G & q = f1 . q1 )
thus  q1 in the carrier of G ; ::_thesis: q = f1 . q1
f1 . q1 = Conjugate ((b ") ") by A1
.= Conjugate b ;
hence  q = f1 . q1 by A18, A19, A20, Def6; ::_thesis: verum
end;
then  rng f1 = the carrier of (InnAutGroup G) by FUNCT_2:10;
then  f1 is onto by FUNCT_2:def_3;
then  InnAutGroup G = Image f1 by GROUP_6:57;
hence  InnAutGroup G,G ./. (center G) are_isomorphic by A4, GROUP_6:78; ::_thesis: verum
end;

theorem :: AUTGROUP:30
for G being strict Group st G is commutative Group holds
for f being Element of (InnAutGroup G) holds f = 1_ (InnAutGroup G)
proof
let G be strict Group; ::_thesis: ( G is commutative Group implies for f being Element of (InnAutGroup G) holds f = 1_ (InnAutGroup G) )
assume A1: G is commutative Group ; ::_thesis: for f being Element of (InnAutGroup G) holds f = 1_ (InnAutGroup G)
let f be Element of (InnAutGroup G); ::_thesis: f = 1_ (InnAutGroup G)
 the carrier of (InnAutGroup G) = InnAut G by Def5;
then consider f1 being Element of InnAut G such that
A2: f1 = f ;
 f1 is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
then consider a being Element of G such that
A3: for x being Element of G holds f1 . x = x |^ a by Def4;
A4: for x being Element of G holds f1 . x = x
proof
let x be Element of G; ::_thesis: f1 . x = x
thus f1 . x = x |^ a by A3
.= x by A1, GROUP_3:29 ; ::_thesis: verum
end;
 for x being Element of G holds f1 . x = (id the carrier of G) . x
proof
let x be Element of G; ::_thesis: f1 . x = (id the carrier of G) . x
thus f1 . x = x by A4
.= (id the carrier of G) . x by FUNCT_1:18 ; ::_thesis: verum
end;
then  f1 = id the carrier of G by FUNCT_2:63;
hence  f = 1_ (InnAutGroup G) by A2, Th19; ::_thesis: verum
end;