let G be Group; :: thesis: for a, x being Element of G holds
( a * x = x * a iff x is Element of (Centralizer a) )
let a, x be Element of G; :: thesis: ( a * x = x * a iff x is Element of (Centralizer a) )
A1: the carrier of (Centralizer a) = { b where b is Element of G : a * b = b * a } by Def1;

hereby :: thesis: ( x is Element of (Centralizer a) implies a * x = x * a )

assume a * x = x * a ; :: thesis: x is Element of (Centralizer a)
then x in the carrier of (Centralizer a) by A1;
hence x is Element of (Centralizer a) ; :: thesis: verum

end;

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