let R be Skew-Field; :: thesis: for s, a being Element of R holds
( a in the carrier of (centralizer s) iff a * s = s * a )
let s, a be Element of R; :: thesis: ( a in the carrier of (centralizer s) iff a * s = s * a )
set cs = centralizer s;
set ccs = the carrier of (centralizer s);
A1: the carrier of (centralizer s) = { x where x is Element of R : x * s = s * x } by Def5;

hereby :: thesis: ( a * s = s * a implies a in the carrier of (centralizer s) )

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

end;

assume a * s = s * a ; :: thesis: a in the carrier of (centralizer s)
hence a in the carrier of (centralizer s) by A1; :: thesis: verum