the carrier of (MultGroup R) = NonZero R by Def1;
hence MultGroup R is finite ; :: thesis: verum