let R be finite Skew-Field; :: thesis: card the carrier of (center (MultGroup R)) = (card the carrier of (center R)) - 1
A1: the carrier of (MultGroup R) = NonZero R by UNIROOTS:def 1;
the carrier of (center (MultGroup R)) c= the carrier of (MultGroup R) by GROUP_2:def 5;
then A2: not 0. R in the carrier of (center (MultGroup R)) by A1, ZFMISC_1:56;
the carrier of (center R) = the carrier of (center (MultGroup R)) \/ {(0. R)} by Th22;
then card the carrier of (center R) = (card the carrier of (center (MultGroup R))) + 1 by A2, CARD_2:41;
hence card the carrier of (center (MultGroup R)) = (card the carrier of (center R)) - 1 ; :: thesis: verum