let R be Ring; :: thesis: for r being Element of R st r in center (UnitGroup R) holds
for s being Element of R st s in UnitGroup R holds
r * s = s * r
let r be Element of R; :: thesis: ( r in center (UnitGroup R) implies for s being Element of R st s in UnitGroup R holds
r * s = s * r )
assume A1: r in center (UnitGroup R) ; :: thesis: for s being Element of R st s in UnitGroup R holds
r * s = s * r
then reconsider r9 = r as Element of (UnitGroup R) by GROUP_2:40, STRUCT_0:def 5;
let s be Element of R; :: thesis: ( s in UnitGroup R implies r * s = s * r )
assume s in UnitGroup R ; :: thesis: r * s = s * r
then reconsider s9 = s as Element of (UnitGroup R) by STRUCT_0:def 5;
thus r * s = r9 * s9 by Th110
.= s9 * r9 by A1, GROUP_5:77
.= s * r by Th110 ; :: thesis: verum