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