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
() . q in K2
proof
let q be set ; :: thesis: ( q in [:K2,K2:] implies () . q in K2 )
assume q in [:K2,K2:] ; :: thesis: () . q in K2
then consider x, y being object 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;
() . q = () . (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 = () || () as BinOp of () by REALSET1:6;
set IG = multMagma(# (),op #);
A4: now :: thesis: for x, y being Element of multMagma(# (),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(# (),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 [:(),():] by ZFMISC_1:def 2;
assume ( x = f & y = g ) ; :: thesis: x * y = f * g
hence x * y = () . (f,g) by
.= f * g by Th14 ;
:: thesis: verum
end;
A6: for f, g, h being Element of multMagma(# (),op #) holds (f * g) * h = f * (g * h)
proof
let f, g, h be Element of multMagma(# (),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(# (),op #) st
for h being Element of multMagma(# (),op #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (),op #) st
( h * g = e & g * h = e ) )
proof
reconsider e = id the carrier of G as Element of multMagma(# (),op #) by Th15;
take e ; :: thesis: for h being Element of multMagma(# (),op #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (),op #) st
( h * g = e & g * h = e ) )

let h be Element of multMagma(# (),op #); :: thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (),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(# (),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(# (),op #) st
( h * g = e & g * h = e )

reconsider g = A " as Element of multMagma(# (),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 ;
thus h * g = A * (A ") by A4, A8
.= e by ; :: thesis: g * h = e
thus g * h = (A ") * A by A4, A8
.= e by ; :: thesis: verum
end;
then reconsider IG = multMagma(# (),op #) as Group by ;
the carrier of IG c= the carrier of () by Th13;
then reconsider IG = IG as strict Subgroup of AutGroup G by GROUP_2:def 5;
for f, k being Element of () st k is Element of IG holds
k |^ f in IG
proof
let f, k be Element of (); :: 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 ;
((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 ;
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 ;
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
.= ((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
.= y |^ (A . a) by GROUP_6:32 ; :: thesis: verum
end;
hence ((f1 ") * g1) * f1 is Element of InnAut G by ; :: 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 ;
then C * D = (f ") * k by ;
then q in carr IG by ;
hence k |^ f in IG by ; :: 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