let R be Skew-Field; :: thesis: for s being Element of R
for t being Element of () st t = s holds
the carrier of () = the carrier of () \/ {(0. R)}

let s be Element of R; :: thesis: for t being Element of () st t = s holds
the carrier of () = the carrier of () \/ {(0. R)}

let t be Element of (); :: thesis: ( t = s implies the carrier of () = the carrier of () \/ {(0. R)} )
assume A1: t = s ; :: thesis: the carrier of () = the carrier of () \/ {(0. R)}
set ct = Centralizer t;
set cs = centralizer s;
set cct = the carrier of ();
set ccs = the carrier of ();
A2: the carrier of () = NonZero R by UNIROOTS:def 1;
A3: the carrier of () = { b where b is Element of () : t * b = b * t } by Def1;
A4: the carrier of () = { 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 () implies x in the carrier of () \/ {(0. R)} ) & ( x in the carrier of () \/ {(0. R)} implies x in the carrier of () ) )
let x be object ; :: thesis: ( ( x in the carrier of () implies x in the carrier of () \/ {(0. R)} ) & ( x in the carrier of () \/ {(0. R)} implies b1 in the carrier of () ) )
hereby :: thesis: ( x in the carrier of () \/ {(0. R)} implies b1 in the carrier of () )
assume x in the carrier of () ; :: thesis: x in the carrier of () \/ {(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 () \/ {(0. R)}
then c in {(0. R)} by TARSKI:def 1;
hence x in the carrier of () \/ {(0. R)} by ; :: thesis: verum
end;
suppose c <> 0. R ; :: thesis: x in the carrier of () \/ {(0. R)}
then not c in {(0. R)} by TARSKI:def 1;
then reconsider c1 = c as Element of () by ;
t * c1 = s * c by
.= c1 * t by ;
then c in the carrier of () by A3;
hence x in the carrier of () \/ {(0. R)} by ; :: thesis: verum
end;
end;
end;
assume A7: x in the carrier of () \/ {(0. R)} ; :: thesis: b1 in the carrier of ()
per cases ( x in the carrier of () or x in {(0. R)} ) by ;
suppose x in the carrier of () ; :: thesis: b1 in the carrier of ()
then consider b being Element of () 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
.= s * b1 by ;
hence x in the carrier of () by A4, A8; :: thesis: verum
end;
suppose x in {(0. R)} ; :: thesis: b1 in the carrier of ()
then A10: x = 0. R by TARSKI:def 1;
(0. R) * s = s * (0. R) ;
hence x in the carrier of () by ; :: thesis: verum
end;
end;
end;
hence the carrier of () = the carrier of () \/ {(0. R)} by TARSKI:2; :: thesis: verum