let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
not k Pencils_of V is empty
let V be finite-dimensional VectSp of F; :: thesis: for k being Nat st 1 <= k & k < dim V holds
not k Pencils_of V is empty
let k be Nat; :: thesis: ( 1 <= k & k < dim V implies not k Pencils_of V is empty )
assume A1: ( 1 <= k & k < dim V ) ; :: thesis: not k Pencils_of V is empty
then k + 1 <= dim V by NAT_1:13;
then consider W2 being strict Subspace of V such that
A2: dim W2 = k + 1 by VECTSP_9:39;
k -' 1 <= k by NAT_D:35;
then k -' 1 <= dim W2 by A2, NAT_1:13;
then consider W1 being strict Subspace of W2 such that
A3: dim W1 = k -' 1 by VECTSP_9:39;
A4: (dim W1) + 1 = k by A1, A3, XREAL_1:237;
reconsider W1' = W1 as Subspace of V by VECTSP_4:34;
pencil W1',W2,k in k Pencils_of V by A2, A4, Def4;
hence not k Pencils_of V is empty ; :: thesis: verum