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

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