let R be Ring; :: thesis: for x being object st x in center R & x in UnitGroup R holds
x in center (UnitGroup R)
let x be object ; :: thesis: ( x in center R & x in UnitGroup R implies x in center (UnitGroup R) )
assume A1: x in center R ; :: thesis: ( not x in UnitGroup R or x in center (UnitGroup R) )
assume x in UnitGroup R ; :: thesis: x in center (UnitGroup R)
then reconsider a = x as Element of (UnitGroup R) by STRUCT_0:def 5;
for g being Element of (UnitGroup R) holds a * g = g * a

proof

let g be Element of (UnitGroup R); :: thesis: a * g = g * a
( a in units R & g in units R ) ;
then reconsider g9 = g, a9 = a as Element of R ;
thus a * g = a9 * g9 by Th110
.= g9 * a9 by A1, WEDDWITT:43
.= g * a by Th110 ; :: thesis: verum

end;

hence x in center (UnitGroup R) by GROUP_5:77; :: thesis: verum