for R being finite Skew-Field
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