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;
set B = the Basis of (VectSp_over_center R);
the Basis of (VectSp_over_center R) is finite by A1;
then VectSp_over_center R is finite-dimensional by MATRLIN:def 1;
hence card the carrier of R = (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by A1, Th15; :: thesis: verum