let R be finite Skew-Field; :: thesis: card (MultGroup R) = (card R) - 1
set G = MultGroup R;
the carrier of (MultGroup R) = NonZero R by Def1;
then card the carrier of (MultGroup R) = (card R) - (card {(0. R)}) by CARD_2:44;
hence card (MultGroup R) = (card R) - 1 by CARD_1:30; :: thesis: verum