let R be finite Skew-Field; :: thesis: for r being Element of R st r is Element of (MultGroup R) holds
((card the carrier of (center R)) |^ (dim (VectSp_over_center r))) - 1 divides ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1
let r be Element of R; :: thesis: ( r is Element of (MultGroup R) implies ((card the carrier of (center R)) |^ (dim (VectSp_over_center r))) - 1 divides ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 )
assume A1: r is Element of (MultGroup R) ; :: thesis: ((card the carrier of (center R)) |^ (dim (VectSp_over_center r))) - 1 divides ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1
set G = MultGroup R;
set q = card the carrier of (center R);
set qr = card the carrier of (centralizer r);
set n = dim (VectSp_over_center R);
reconsider s = r as Element of (MultGroup R) by A1;
card R = (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by Th31;
then card (MultGroup R) = ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 by UNIROOTS:18;
then ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 = (card (con_class s)) * (card (Centralizer s)) by Th13;
then card (Centralizer s) divides ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 by INT_1:def 3;
then (card the carrier of (centralizer r)) - 1 divides ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 by Th30;
hence ((card the carrier of (center R)) |^ (dim (VectSp_over_center r))) - 1 divides ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 by Th33; :: thesis: verum