reconsider K1 = Aut G as set ;
reconsider K2 = InnAut G as Subset of K1 by Th14;
for q being set st q in [:K2,K2:] holds
(AutComp G) . q in K2

proof

let q be set ; :: thesis:
assume q in [:K2,K2:] ; :: thesis:
then consider x, y being set such that
A1: ( x in K2 & y in K2 & q = [x,y] ) by ZFMISC_1:def 2;
reconsider x = x, y = y as Element of InnAut G by A1;
A2: x * y is Element of InnAut G by Th18;
(AutComp G) . q = (AutComp G) . x,y by A1
.= x * y by Th15 ;
hence (AutComp G) . q in K2 by A2; :: thesis:

end;

then AutComp G is Presv of K1,K2 by REALSET1:def 6;
then reconsider op = (AutComp G) || (InnAut G) as BinOp of (InnAut G) by REALSET1:9;
set IG = multMagma(# (InnAut G),op #);
( multMagma(# (InnAut G),op #) is associative & multMagma(# (InnAut G),op #) is Group-like )

proof

A3: now

let x, y be Element of multMagma(# (InnAut G),op #); :: thesis:
let f, g be Element of InnAut G; :: thesis:
assume A4: ( x = f & y = g ) ; :: thesis:
[f,g] in [:(InnAut G),(InnAut G):] by ZFMISC_1:def 2;
hence x * y = (AutComp G) . f,g by A4, FUNCT_1:72
.= f * g by Th15 ;
:: thesis:

end;

thus for f, g, h being Element of multMagma(# (InnAut G),op #) holds (f * g) * h = f * (g * h) :: according to GROUP_1:def 4 :: thesis:

proof

let f, g, h be Element of multMagma(# (InnAut G),op #); :: thesis:
reconsider A = f, B = g, C = h as Element of InnAut G ;
A5: f * g = A * B by A3;
A6: g * h = B * C by A3;
thus (f * g) * h = (A * B) * C by A3, A5
.= A * (B * C) by RELAT_1:55
.= f * (g * h) by A3, A6 ; :: thesis:

end;

thus 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 ) ) :: according to GROUP_1:def 3 :: thesis:

proof

reconsider e = id the carrier of G as Element of multMagma(# (InnAut G),op #) by Th16;
take e ; :: thesis:
let h be Element of multMagma(# (InnAut G),op #); :: thesis:
consider A being Element of InnAut G such that
A7: A = h ;
h * e = A * (id the carrier of G) by A3, A7
.= A by FUNCT_2:23 ;
hence h * e = h by A7; :: thesis:
e * h = (id the carrier of G) * A by A3, A7
.= A by FUNCT_2:23 ;
hence e * h = h by A7; :: thesis:
reconsider g = A " as Element of multMagma(# (InnAut G),op #) by Th17;
take g ; :: thesis:
reconsider A = A as Element of Aut G by Th13;
reconsider A = A as Homomorphism of G,G by Def1;
A8: ( A is one-to-one & A is onto ) by Def1;
then A9: rng A = the carrier of G by FUNCT_2:def 3;
thus h * g = A * (A " ) by A3, A7
.= e by A8, A9, FUNCT_2:35 ; :: thesis:
thus g * h = (A " ) * A by A3, A7
.= e by A8, A9, FUNCT_2:35 ; :: thesis:

end;

then reconsider IG = multMagma(# (InnAut G),op #) as Group ;
IG is Subgroup of AutGroup G

proof

the carrier of IG c= the carrier of (AutGroup G) by Th14;
hence IG is Subgroup of AutGroup G by GROUP_2:def 5; :: thesis:

end;

then reconsider IG = IG as strict Subgroup of AutGroup G ;
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:
assume A10: k is Element of IG ; :: thesis:
consider f1 being Element of Aut G such that
A11: f1 = f ;
consider g being Element of InnAut G such that
A12: g = k by A10;
g is Element of Aut G by Th13;
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:11;
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:31;
then (f1 " ) * g1 is Function of the carrier of G,the carrier of G by FUNCT_2:19;
then ((f1 " ) * g1) * f1 is Function of the carrier of G,the carrier of G by FUNCT_2:19;
then A17: ((f1 " ) * g1) * f1 is Element of Funcs the carrier of G,the carrier of G by FUNCT_2:11;
f1 " is Element of Aut G by Th7;
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:35;

now

let y be Element of G; :: thesis:
thus (((f1 " ) * g1) * f1) . y = ((f1 " ) * (g1 * f1)) . y by RELAT_1:55
.= (f1 " ) . ((g1 * f1) . y) by FUNCT_2:21
.= (f1 " ) . (g1 . (f1 . y)) by FUNCT_2:21
.= (f1 " ) . ((f1 . y) |^ a) by A14
.= (A . ((a " ) * (f1 . y))) * (A . a) by A18, GROUP_6:def 7
.= ((A . (a " )) * (A . (f1 . y))) * (A . a) by GROUP_6:def 7
.= ((A . (a " )) * ((A * f1) . y)) * (A . a) by FUNCT_2:21
.= ((A . (a " )) * y) * (A . a) by A19, FUNCT_1:35
.= y |^ (A . a) by GROUP_6:41 ; :: thesis:

end;

hence ((f1 " ) * g1) * f1 is Element of InnAut G by A17, Def4; :: thesis:

end;

then A20: ((f1 " ) * g) * f1 in InnAut G by A13;
reconsider C = f1 " as Element of Aut G by Th7;
reconsider D = g as Element of Aut G by Th13;
f1 " = f " by A11, Th11;
then A21: C * D = (f " ) * k by A12, Def2;
consider q being set such that
A22: q = ((f " ) * k) * f ;
q in carr IG by A11, A20, A21, A22, Def2;
hence k |^ f in IG by A22, STRUCT_0:def 5; :: thesis:

end;

then reconsider IG = IG as strict normal Subgroup of AutGroup G by Lm1;
take IG ; :: thesis:
thus the carrier of IG = InnAut G ; :: thesis: