let R be finite Skew-Field; :: thesis: 0 < dim (VectSp_over_center R)
set q = card the carrier of (center R);
set n = dim (VectSp_over_center R);
set Rs = MultGroup R;
card R = (card the carrier of (center R)) |^ (dim (VectSp_over_center R)) by Th31;
then A1: card (MultGroup R) = ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1 by UNIROOTS:18;

now :: thesis: not dim (VectSp_over_center R) = 0

assume A2: dim (VectSp_over_center R) = 0 ; :: thesis: contradiction
(card the carrier of (center R)) |^ (dim (VectSp_over_center R)) = (card the carrier of (center R)) #Z (dim (VectSp_over_center R)) by PREPOWER:36;
then card (MultGroup R) = 1 - 1 by A1, A2, PREPOWER:34;
hence contradiction by GROUP_1:45; :: thesis: verum

end;

hence 0 < dim (VectSp_over_center R) ; :: thesis: verum