let G be Group; :: thesis: InnAutGroup G,G ./. (center G) are_isomorphic
deffunc H₁( 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 = H₁(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 object ; :: 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 ;
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 object ; :: 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 by A15, A14;
then g = id the carrier of G ;
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 object st q in the carrier of (InnAutGroup G) holds
ex q1 being object st
( q1 in the carrier of G & q = f1 . q1 )

proof

let q be object ; :: thesis: ( q in the carrier of (InnAutGroup G) implies ex q1 being object st
( q1 in the carrier of G & q = f1 . q1 ) )
assume A17: q in the carrier of (InnAutGroup G) ; :: thesis: ex q1 being object 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 ;
then InnAutGroup G = Image f1 by GROUP_6:57;
hence InnAutGroup G,G ./. (center G) are_isomorphic by A4, GROUP_6:78; :: thesis: verum