let R be finite Skew-Field; :: thesis: for s being Element of holds 0 < dim (VectSp_over_center s)
let s be Element of ; :: thesis: 0 < dim (VectSp_over_center s)
set q = card the carrier of (center R);
set ns = dim (VectSp_over_center s);

now

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:46;
then (card the carrier of (center R)) |^ (dim (VectSp_over_center s)) = 1 by A1, PREPOWER:44;
then card the carrier of (centralizer s) = 1 by Th34;
hence contradiction by Th29; :: thesis: verum

end;

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