let G be Group; :: thesis: center G is characteristic Subgroup of G
set Z = center G;
A1: for phi being Automorphism of G
for y, z being Element of G st z in center G holds
(phi . z) * y = y * (phi . z)

proof

let phi be Automorphism of G; :: thesis: for y, z being Element of G st z in center G holds
(phi . z) * y = y * (phi . z)
let y, z be Element of G; :: thesis: ( z in center G implies (phi . z) * y = y * (phi . z) )
assume B1: z in center G ; :: thesis: (phi . z) * y = y * (phi . z)
set x = (phi ") . y;
(phi . z) * y = (phi . z) * (phi . ((phi ") . y)) by Th4
.= phi . (z * ((phi ") . y)) by GROUP_6:def 6
.= phi . (((phi ") . y) * z) by B1, GROUP_5:77
.= (phi . ((phi ") . y)) * (phi . z) by GROUP_6:def 6
.= y * (phi . z) by Th4 ;
hence (phi . z) * y = y * (phi . z) ; :: thesis: verum

end;

A2: for phi being Automorphism of G
for z being Element of G st z in center G holds
(phi | (center G)) . z in center G

proof

let phi be Automorphism of G; :: thesis: for z being Element of G st z in center G holds
(phi | (center G)) . z in center G
let z be Element of G; :: thesis: ( z in center G implies (phi | (center G)) . z in center G )
assume B1: z in center G ; :: thesis: (phi | (center G)) . z in center G
then for y being Element of G holds (phi . z) * y = y * (phi . z) by A1;
then phi . z in center G by GROUP_5:77;
hence (phi | (center G)) . z in center G by B1, Th1; :: thesis: verum

end;

for phi being Automorphism of G holds Image (phi | (center G)) is Subgroup of center G

proof

let phi be Automorphism of G; :: thesis: Image (phi | (center G)) is Subgroup of center G
for w being Element of G st w in rng (phi | (center G)) holds
w in center G

proof

let w be Element of G; :: thesis: ( w in rng (phi | (center G)) implies w in center G )
assume w in rng (phi | (center G)) ; :: thesis: w in center G
then consider z being object such that
C1: z in dom (phi | (center G)) and
C2: (phi | (center G)) . z = w by FUNCT_1:def 3;
reconsider z = z as Element of (center G) by C1;
z is Element of G by GROUP_2:42;
hence w in center G by C2, A2, STRUCT_0:def 5; :: thesis: verum

end;

then rng (phi | (center G)) c= the carrier of (center G) by STRUCT_0:def 5;
then the carrier of (Image (phi | (center G))) c= the carrier of (center G) by GROUP_6:44;
hence Image (phi | (center G)) is Subgroup of center G by GROUP_2:57; :: thesis: verum

end;

hence center G is characteristic Subgroup of G by Th40; :: thesis: verum