theorem Th17: :: UNIROOTS:17

for R being Skew-Field holds 1_ R = 1_ (MultGroup R)