let R be Skew-Field; :: thesis: for s, a, b being Element of R st a in the carrier of (center R) & b in the carrier of (centralizer s) holds

a * b in the carrier of (centralizer s)

let s, a, b be Element of R; :: thesis: ( a in the carrier of (center R) & b in the carrier of (centralizer s) implies a * b in the carrier of (centralizer s) )

assume that

A1: a in the carrier of (center R) and

A2: b in the carrier of (centralizer s) ; :: thesis: a * b in the carrier of (centralizer s)

set cs = centralizer s;

set ccs = the carrier of (centralizer s);

A3: the carrier of (centralizer s) = { x where x is Element of R : x * s = s * x } by Def5;

A4: a in center R by A1;

(a * b) * s = a * (b * s) by GROUP_1:def 3

.= (b * s) * a by A4, Th17

.= (s * b) * a by A2, Th24

.= s * (b * a) by GROUP_1:def 3

.= s * (a * b) by A4, Th17 ;

hence a * b in the carrier of (centralizer s) by A3; :: thesis: verum

a * b in the carrier of (centralizer s)

let s, a, b be Element of R; :: thesis: ( a in the carrier of (center R) & b in the carrier of (centralizer s) implies a * b in the carrier of (centralizer s) )

assume that

A1: a in the carrier of (center R) and

A2: b in the carrier of (centralizer s) ; :: thesis: a * b in the carrier of (centralizer s)

set cs = centralizer s;

set ccs = the carrier of (centralizer s);

A3: the carrier of (centralizer s) = { x where x is Element of R : x * s = s * x } by Def5;

A4: a in center R by A1;

(a * b) * s = a * (b * s) by GROUP_1:def 3

.= (b * s) * a by A4, Th17

.= (s * b) * a by A2, Th24

.= s * (b * a) by GROUP_1:def 3

.= s * (a * b) by A4, Th17 ;

hence a * b in the carrier of (centralizer s) by A3; :: thesis: verum