let R be Skew-Field; :: thesis: the carrier of (center R) = the carrier of (center (MultGroup R)) \/ {(0. R)}
A1: the carrier of (center (MultGroup R)) c= the carrier of (MultGroup R) by GROUP_2:def 5;
A2: the carrier of (MultGroup R) = NonZero R by UNIROOTS:def 1;
A3: the carrier of (MultGroup R) \/ {(0. R)} = the carrier of R by UNIROOTS:15;
A4: the carrier of (center R) c= the carrier of R by Th16;
A5: the carrier of (center (MultGroup R)) \/ {(0. R)} c= the carrier of (center R)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (center (MultGroup R)) \/ {(0. R)} or x in the carrier of (center R) )
assume A6: x in the carrier of (center (MultGroup R)) \/ {(0. R)} ; :: thesis: x in the carrier of (center R)

per cases ( x in the carrier of (center (MultGroup R)) or x in {(0. R)} ) by A6, XBOOLE_0:def 3;

suppose A7: x in the carrier of (center (MultGroup R)) ; :: thesis: x in the carrier of (center R)

then reconsider a = x as Element of (MultGroup R) by A1;
A8: a in center (MultGroup R) by A7;
reconsider a1 = a as Element of R by UNIROOTS:19;

now :: thesis: for b being Element of R holds a1 * b = b * a1

let b be Element of R; :: thesis: a1 * b = b * a1
thus a1 * b = b * a1 :: thesis: verum

proof

per cases ( b in the carrier of (MultGroup R) or b in {(0. R)} ) by A3, XBOOLE_0:def 3;

suppose b in the carrier of (MultGroup R) ; :: thesis: a1 * b = b * a1

then reconsider b1 = b as Element of (MultGroup R) ;
thus a1 * b = a * b1 by UNIROOTS:16
.= b1 * a by A8, GROUP_5:77
.= b * a1 by UNIROOTS:16 ; :: thesis: verum

end;

suppose b in {(0. R)} ; :: thesis: a1 * b = b * a1

then A9: b = 0. R by TARSKI:def 1;
hence a1 * b = 0. R
.= b * a1 by A9 ;
:: thesis: verum

end;

end;

end;

end;

then a1 in center R by Th17;
hence x in the carrier of (center R) ; :: thesis: verum

end;

suppose x in {(0. R)} ; :: thesis: x in the carrier of (center R)

then x = 0. R by TARSKI:def 1;
then x in center R by Th18;
hence x in the carrier of (center R) ; :: thesis: verum

end;

end;

end;

the carrier of (center R) c= the carrier of (center (MultGroup R)) \/ {(0. R)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (center R) or x in the carrier of (center (MultGroup R)) \/ {(0. R)} )
assume A10: x in the carrier of (center R) ; :: thesis: x in the carrier of (center (MultGroup R)) \/ {(0. R)}
then reconsider a = x as Element of (center R) ;
reconsider a1 = a as Element of R by A4;

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

suppose a1 = 0. R ; :: thesis: x in the carrier of (center (MultGroup R)) \/ {(0. R)}

then a1 in {(0. R)} by TARSKI:def 1;
hence x in the carrier of (center (MultGroup R)) \/ {(0. R)} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose a1 <> 0. R ; :: thesis: x in the carrier of (center (MultGroup R)) \/ {(0. R)}

then not a1 in {(0. R)} by TARSKI:def 1;
then reconsider a2 = a1 as Element of (MultGroup R) by A2, XBOOLE_0:def 5;

now :: thesis: for b being Element of (MultGroup R) holds a2 * b = b * a2

let b be Element of (MultGroup R); :: thesis: a2 * b = b * a2
b in the carrier of (MultGroup R) ;
then reconsider b1 = b as Element of R by A2;
A11: x in center R by A10;
thus a2 * b = a1 * b1 by UNIROOTS:16
.= b1 * a1 by A11, Th17
.= b * a2 by UNIROOTS:16 ; :: thesis: verum

end;

then a1 in center (MultGroup R) by GROUP_5:77;
then a1 in the carrier of (center (MultGroup R)) ;
hence x in the carrier of (center (MultGroup R)) \/ {(0. R)} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence the carrier of (center R) = the carrier of (center (MultGroup R)) \/ {(0. R)} by A5, XBOOLE_0:def 10; :: thesis: verum