let G be Group; :: thesis: for K being strict characteristic Subgroup of G holds Centralizer K is characteristic Subgroup of G
let K be strict characteristic Subgroup of G; :: thesis: Centralizer K is characteristic Subgroup of G
for phi being Automorphism of G
for x being Element of G st x in Centralizer K holds
phi . x in Centralizer K

proof

let phi be Automorphism of G; :: thesis: for x being Element of G st x in Centralizer K holds
phi . x in Centralizer K
let x be Element of G; :: thesis: ( x in Centralizer K implies phi . x in Centralizer K )
assume B1: x in Centralizer K ; :: thesis: phi . x in Centralizer K
set y = phi . x;
reconsider psi = phi " as Automorphism of G by GROUP_6:62;
for k being Element of G st k in K holds
(phi . x) * k = k * (phi . x)

proof

let k be Element of G; :: thesis: ( k in K implies (phi . x) * k = k * (phi . x) )
assume C1: k in K ; :: thesis: (phi . x) * k = k * (phi . x)
set j = psi . k;
phi . (x * (psi . k)) = phi . ((psi . k) * x) by B1, C1, Th50, Th60
.= (phi . (psi . k)) * (phi . x) by GROUP_6:def 6 ;
then (phi . x) * (phi . (psi . k)) = (phi . (psi . k)) * (phi . x) by GROUP_6:def 6
.= k * (phi . x) by Th4 ;
hence (phi . x) * k = k * (phi . x) by Th4; :: thesis: verum

end;

then phi . x is Element of (Centralizer K) by Th60;
hence phi . x in Centralizer K ; :: thesis: verum

end;

hence Centralizer K is characteristic Subgroup of G by Th50; :: thesis: verum