let G be strict Group; :: thesis:
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;

let a, b be Element of G; :: thesis:
A2: f . (a * b) = Conjugate ((a * b) ") by A1
.= Conjugate ((b ") * (a ")) by GROUP_1:17
.= (Conjugate (a ")) * (Conjugate (b ")) by Th21 ;

let A, B be Element of (InnAutGroup G); :: thesis:
assume A3: ( A = f . a & B = f . b ) ; :: thesis:
then ( A = Conjugate (a ") & B = Conjugate (b ") ) by A1;
hence f . (a * b) = (f . a) * (f . b) by A2, A3, Th18; :: thesis:

end;

hence f . (a * b) = (f . a) * (f . b) ; :: thesis:

end;

then reconsider f1 = f as Homomorphism of G,(InnAutGroup G) by GROUP_6:def 6;
A4: Ker f1 = center G

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 }

let q be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: q in the carrier of (Ker f1) ; :: thesis:
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

let b be Element of G; :: thesis:
(id the carrier of G) . b = b ;
hence (Conjugate (x ")) . b = b by A1, A9; :: thesis:

end;

let b be Element of G; :: thesis:
(Conjugate (x ")) . b = b |^ (x ") by Def6;
hence b |^ (x ") = b by A10; :: thesis:

end;

for b being Element of G holds x * b = b * x

let b be Element of G; :: thesis:
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:

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:

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)

let q be object ; :: according to TARSKI:def 3 :: thesis:
assume q in { a where a is Element of G : for b being Element of G holds a * b = b * a } ; :: thesis:
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

let b be Element of G; :: thesis:
(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:

end;

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:

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 )

let q be object ; :: thesis:
assume A17: q in the carrier of (InnAutGroup G) ; :: thesis:
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:
thus q1 in the carrier of G ; :: thesis:
f1 . q1 = Conjugate ((b ") ") by A1
.= Conjugate b ;
hence q = f1 . q1 by A18, A19, A20, Def6; :: thesis:

end;