let GF be Field; :: thesis: for n being Nat
for V being finite-dimensional VectSp of GF st n <= dim V holds
ex W being strict Subspace of V st dim W = n
let n be Nat; :: thesis: for V being finite-dimensional VectSp of GF st n <= dim V holds
ex W being strict Subspace of V st dim W = n
let V be finite-dimensional VectSp of GF; :: thesis: ( n <= dim V implies ex W being strict Subspace of V st dim W = n )
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def 1;
assume n <= dim V ; :: thesis: ex W being strict Subspace of V st dim W = n
then n <= card I by A1, Def1;
then consider A being finite Subset of I such that
A2: card A = n by FINSEQ_4:72;
reconsider A = A as Subset of V by XBOOLE_1:1;
reconsider W = Lin A as strict finite-dimensional Subspace of V ;
I is linearly-independent by A1, VECTSP_7:def 3;
then dim W = n by A2, Th26, VECTSP_7:1;
hence ex W being strict Subspace of V st dim W = n ; :: thesis: verum