theorem Th17: :: UNIROOTS:17
for R being Skew-Field holds 1_ R = 1_ (MultGroup R)