let R be Skew-Field; :: thesis:
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:
assume A6: x in the carrier of (center (MultGroup R)) \/ {(0. R)} ; :: thesis:

per cases by A6, XBOOLE_0:def 3;

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

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:

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

proof

per cases by A3, XBOOLE_0:def 3;

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

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:

end;

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

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

end;

end;

end;

end;

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

end;

suppose x in {(0. R)} ; :: thesis:

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

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:
assume A10: x in the carrier of (center R) ; :: thesis:
then reconsider a = x as Element of (center R) ;
reconsider a1 = a as Element of R by A4;

per cases ;

suppose a1 = 0. R ; :: thesis:

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:

end;

suppose a1 <> 0. R ; :: thesis:

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:

let b be Element of (MultGroup R); :: thesis:
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:

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:

end;

end;

end;

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