let R be finite Skew-Field; :: thesis: for s being Element of R holds card the carrier of (centralizer s) = (card the carrier of (center R)) |^ (dim (VectSp_over_center s))
let s be Element of R; :: thesis: card the carrier of (centralizer s) = (card the carrier of (center R)) |^ (dim (VectSp_over_center s))
set vR = VectSp_over_center s;
A1: addLoopStr(# the carrier of (VectSp_over_center s), the addF of (VectSp_over_center s), the ZeroF of (VectSp_over_center s) #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) by Def7;
set B = the Basis of (VectSp_over_center s);
the Basis of (VectSp_over_center s) is finite by A1;
then VectSp_over_center s is finite-dimensional by MATRLIN:def 1;
hence card the carrier of (centralizer s) = (card the carrier of (center R)) |^ (dim (VectSp_over_center s)) by A1, Th15; :: thesis: verum