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

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

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

end;

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