let R be Skew-Field; :: thesis: for s being Element of R holds the carrier of (centralizer s) c= the carrier of R

let s be Element of R; :: thesis: the carrier of (centralizer s) c= the carrier of R

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;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (centralizer s) or x in the carrier of R )

assume x in the carrier of (centralizer s) ; :: thesis: x in the carrier of R

then ex a being Element of R st

( a = x & a * s = s * a ) by A1;

hence x in the carrier of R ; :: thesis: verum

let s be Element of R; :: thesis: the carrier of (centralizer s) c= the carrier of R

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;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (centralizer s) or x in the carrier of R )

assume x in the carrier of (centralizer s) ; :: thesis: x in the carrier of R

then ex a being Element of R st

( a = x & a * s = s * a ) by A1;

hence x in the carrier of R ; :: thesis: verum