let R be Skew-Field; :: thesis: MultGroup R = UnitGroup R
the carrier of (MultGroup R) = NonZero R by UNIROOTS:def 1
.= the carrier of (UnitGroup R) by Th116 ;
hence MultGroup R = UnitGroup R by UNIROOTS:def 1; :: thesis: verum