let R be finite Skew-Field; :: thesis: for s being Element of R holds 0 < dim (VectSp_over_center s)
let s be Element of R; :: thesis: 0 < dim (VectSp_over_center s)
set q = card the carrier of (center R);
set ns = dim (VectSp_over_center s);
now :: thesis: not dim (VectSp_over_center s) = 0
assume A1: dim (VectSp_over_center s) = 0 ; :: thesis: contradiction
(card the carrier of (center R)) |^ (dim (VectSp_over_center s)) = (card the carrier of (center R)) #Z (dim (VectSp_over_center s)) by PREPOWER:36;
then (card the carrier of (center R)) |^ (dim (VectSp_over_center s)) = 1 by A1, PREPOWER:34;
then card the carrier of (centralizer s) = 1 by Th33;
hence contradiction by Th28; :: thesis: verum
end;
hence 0 < dim (VectSp_over_center s) ; :: thesis: verum