let F be Field; 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; for k being Nat st 1 <= k & k < dim V holds
not k Pencils_of V is empty
let k be Nat; ( 1 <= k & k < dim V implies not k Pencils_of V is empty )
assume that
A1:
1 <= k
and
A2:
k < dim V
; not k Pencils_of V is empty
k + 1 <= dim V
by A2, NAT_1:13;
then consider W2 being strict Subspace of V such that
A3:
dim W2 = k + 1
by VECTSP_9:35;
k -' 1 <= k
by NAT_D:35;
then
k -' 1 <= dim W2
by A3, NAT_1:13;
then consider W1 being strict Subspace of W2 such that
A4:
dim W1 = k -' 1
by VECTSP_9:35;
reconsider W19 = W1 as Subspace of V by VECTSP_4:26;
(dim W1) + 1 = k
by A1, A4, XREAL_1:235;
then
pencil (W19,W2,k) in k Pencils_of V
by A3, Def4;
hence
not k Pencils_of V is empty
; verum