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

then reconsider op = (AutComp G) || (InnAut G) as BinOp of (InnAut G) by REALSET1:6;

set IG = multMagma(# (InnAut G),op #);

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 ) )

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

take IG ; :: thesis: the carrier of IG = InnAut G

thus the carrier of IG = InnAut G ; :: thesis: verum

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

then
AutComp G is Presv of K1,K2
by REALSET1:def 4;
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 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;

(AutComp G) . q = (AutComp G) . (x,y) by A2

.= x * y by Th14 ;

hence (AutComp G) . q in K2 by A3; :: thesis: verum

end;assume q in [:K2,K2:] ; :: thesis: (AutComp G) . 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;

(AutComp G) . q = (AutComp G) . (x,y) by A2

.= x * y by Th14 ;

hence (AutComp G) . q in K2 by A3; :: thesis: verum

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

A6:
for f, g, h being Element of multMagma(# (InnAut G),op #) holds (f * g) * h = f * (g * h)
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;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

proof

ex e being Element of multMagma(# (InnAut G),op #) st
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;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

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

then reconsider IG = multMagma(# (InnAut G),op #) as Group by A6, GROUP_1:def 2, GROUP_1:def 3;
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 ;

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;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 ;

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

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

then reconsider IG = IG as strict normal Subgroup of AutGroup G by Lm1;
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

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;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

then A20:
((f1 ") * g) * f1 in InnAut G
by A13;
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;

end;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)

hence
((f1 ") * g1) * f1 is Element of InnAut G
by A17, Def4; :: thesis: verumlet 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

.= y |^ (A . a) by GROUP_6:32 ; :: thesis: verum

end;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

.= y |^ (A . a) by GROUP_6:32 ; :: thesis: verum

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

take IG ; :: thesis: the carrier of IG = InnAut G

thus the carrier of IG = InnAut G ; :: thesis: verum