let R be Skew-Field; :: thesis: for s being Element of R
for t being Element of (MultGroup R) st t = s holds
the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}
let s be Element of R; :: thesis: for t being Element of (MultGroup R) st t = s holds
the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}
let t be Element of (MultGroup R); :: thesis: ( t = s implies the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)} )
assume A1: t = s ; :: thesis: the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}
set ct = Centralizer t;
set cs = centralizer s;
set cct = the carrier of (Centralizer t);
set ccs = the carrier of (centralizer s);
A2: the carrier of (MultGroup R) = NonZero R by UNIROOTS:def 1;
A3: the carrier of (Centralizer t) = { b where b is Element of (MultGroup R) : t * b = b * t } by Def1;
A4: the carrier of (centralizer s) = { x where x is Element of R : x * s = s * x } by Def5;

now :: thesis: for x being object holds
( ( x in the carrier of (centralizer s) implies x in the carrier of (Centralizer t) \/ {(0. R)} ) & ( x in the carrier of (Centralizer t) \/ {(0. R)} implies x in the carrier of (centralizer s) ) )

let x be object ; :: thesis: ( ( x in the carrier of (centralizer s) implies x in the carrier of (Centralizer t) \/ {(0. R)} ) & ( x in the carrier of (Centralizer t) \/ {(0. R)} implies b₁ in the carrier of (centralizer s) ) )

hereby :: thesis: ( x in the carrier of (Centralizer t) \/ {(0. R)} implies b₁ in the carrier of (centralizer s) )

assume x in the carrier of (centralizer s) ; :: thesis: x in the carrier of (Centralizer t) \/ {(0. R)}
then consider c being Element of R such that
A5: c = x and
A6: c * s = s * c by A4;

per cases ( c = 0. R or c <> 0. R ) ;

suppose c = 0. R ; :: thesis: x in the carrier of (Centralizer t) \/ {(0. R)}

then c in {(0. R)} by TARSKI:def 1;
hence x in the carrier of (Centralizer t) \/ {(0. R)} by A5, XBOOLE_0:def 3; :: thesis: verum

end;

suppose c <> 0. R ; :: thesis: x in the carrier of (Centralizer t) \/ {(0. R)}

then not c in {(0. R)} by TARSKI:def 1;
then reconsider c1 = c as Element of (MultGroup R) by A2, XBOOLE_0:def 5;
t * c1 = s * c by A1, UNIROOTS:16
.= c1 * t by A1, A6, UNIROOTS:16 ;
then c in the carrier of (Centralizer t) by A3;
hence x in the carrier of (Centralizer t) \/ {(0. R)} by A5, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume A7: x in the carrier of (Centralizer t) \/ {(0. R)} ; :: thesis: b₁ in the carrier of (centralizer s)

per cases ( x in the carrier of (Centralizer t) or x in {(0. R)} ) by A7, XBOOLE_0:def 3;

suppose x in the carrier of (Centralizer t) ; :: thesis: b₁ in the carrier of (centralizer s)

then consider b being Element of (MultGroup R) such that
A8: x = b and
A9: t * b = b * t by A3;
reconsider b1 = b as Element of R by UNIROOTS:19;
b1 * s = t * b by A1, A9, UNIROOTS:16
.= s * b1 by A1, UNIROOTS:16 ;
hence x in the carrier of (centralizer s) by A4, A8; :: thesis: verum

end;

suppose x in {(0. R)} ; :: thesis: b₁ in the carrier of (centralizer s)

then A10: x = 0. R by TARSKI:def 1;
(0. R) * s = s * (0. R) ;
hence x in the carrier of (centralizer s) by A4, A10; :: thesis: verum

end;

end;

end;

hence the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)} by TARSKI:2; :: thesis: verum