the carrier of (MultGroup R) = the carrier of R \ {(0. R)} by Def1;
hence MultGroup R is finite ; :: thesis: verum