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)

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

the carrier of (center R) c= the carrier of (center (MultGroup R)) \/ {(0. R)}
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)

end;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;

end;

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;

hence x in the carrier of (center R) ; :: thesis: verum

end;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

then
a1 in center R
by Th17;let b be Element of R; :: thesis: a1 * b = b * a1

thus a1 * b = b * a1 :: thesis: verum

end;thus a1 * b = b * a1 :: thesis: verum

proof
end;

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

end;

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;thus a1 * b = a * b1 by UNIROOTS:16

.= b1 * a by A8, GROUP_5:77

.= b * a1 by UNIROOTS:16 ; :: thesis: verum

hence x in the carrier of (center R) ; :: thesis: verum

proof

hence
the carrier of (center R) = the carrier of (center (MultGroup R)) \/ {(0. R)}
by A5, XBOOLE_0:def 10; :: thesis: verum
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;

end;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 )
;

end;

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;hence x in the carrier of (center (MultGroup R)) \/ {(0. R)} by XBOOLE_0:def 3; :: thesis: verum

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;

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;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

then
a1 in center (MultGroup R)
by GROUP_5:77;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;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

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