let G be Group; :: thesis: for H being Subgroup of G
for g being Element of G holds
( ( for a being Element of G st a in H holds
g * a = a * g ) iff g is Element of (Centralizer H) )
let H be Subgroup of G; :: thesis: for g being Element of G holds
( ( for a being Element of G st a in H holds
g * a = a * g ) iff g is Element of (Centralizer H) )
let g be Element of G; :: thesis: ( ( for a being Element of G st a in H holds
g * a = a * g ) iff g is Element of (Centralizer H) )
A1: the carrier of (Centralizer H) = { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b } by Th59;

hereby :: thesis: ( g is Element of (Centralizer H) implies for a being Element of G st a in H holds
g * a = a * g )

assume for a being Element of G st a in H holds
g * a = a * g ; :: thesis: g is Element of (Centralizer H)
then g in the carrier of (Centralizer H) by A1;
hence g is Element of (Centralizer H) ; :: thesis: verum

end;

assume g is Element of (Centralizer H) ; :: thesis: for a being Element of G st a in H holds
g * a = a * g
then g in the carrier of (Centralizer H) ;
then ex b being Element of G st
( b = g & ( for a being Element of G st a in H holds
b * a = a * b ) ) by A1;
hence for a being Element of G st a in H holds
g * a = a * g ; :: thesis: verum