let R be finite Skew-Field; :: thesis: card the carrier of R = (card the carrier of (center R)) |^ (dim (VectSp_over_center R))
set vR = VectSp_over_center R;
A1: addLoopStr(# the carrier of (VectSp_over_center R),the addF of (VectSp_over_center R),the ZeroF of (VectSp_over_center R) #) = addLoopStr(# the carrier of R,the addF of R,the ZeroF of R #) by Def6;
consider B being Basis of VectSp_over_center R;
B is finite by A1;
then VectSp_over_center R is finite-dimensional by MATRLIN:def 3;
hence card the carrier of R = (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by A1, Th16; :: thesis: verum