let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial
let V be finite-dimensional VectSp of F; :: thesis: for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial
let W1, W2 be Subspace of V; :: thesis: ( W1 is Subspace of W2 implies for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial )
assume W1 is Subspace of W2 ; :: thesis: for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial
then reconsider U = W1 as Subspace of W2 ;
let k be Nat; :: thesis: ( (dim W1) + 1 = k & dim W2 = k + 1 implies not pencil (W1,W2,k) is trivial )
assume A1: ( (dim W1) + 1 = k & dim W2 = k + 1 ) ; :: thesis: not pencil (W1,W2,k) is trivial
set W = the Linear_Compl of U;
A2: W2 is_the_direct_sum_of the Linear_Compl of U,U by VECTSP_5:def 5;
then A3: the Linear_Compl of U /\ U = (0). W2 by VECTSP_5:def 4;
dim W2 = (dim U) + (dim the Linear_Compl of U) by A2, VECTSP_9:34;
then consider u, v being Vector of the Linear_Compl of U such that
A4: u <> v and
A5: {u,v} is linearly-independent and
(Omega). the Linear_Compl of U = Lin {u,v} by A1, VECTSP_9:31;

A6: now :: thesis: not v in Lin {u}

assume v in Lin {u} ; :: thesis: contradiction
then ex a being Element of F st v = a * u by VECTSP10:3;
hence contradiction by A4, A5, VECTSP_7:5; :: thesis: verum

end;

reconsider u = u, v = v as Vector of W2 by VECTSP_4:10;
reconsider u1 = u, v1 = v as Vector of V by VECTSP_4:10;
A7: v in the Linear_Compl of U ;

A8: now :: thesis: not v in W1

assume v in W1 ; :: thesis: contradiction
then v in (0). W2 by A3, A7, VECTSP_5:3;
then v = 0. W2 by VECTSP_4:35;
then v = 0. the Linear_Compl of U by VECTSP_4:11;
hence contradiction by A5, VECTSP_7:4; :: thesis: verum

end;

A9: u in the Linear_Compl of U ;

A10: now :: thesis: not u in W1

assume u in W1 ; :: thesis: contradiction
then u in (0). W2 by A3, A9, VECTSP_5:3;
then u = 0. W2 by VECTSP_4:35;
then u = 0. the Linear_Compl of U by VECTSP_4:11;
hence contradiction by A5, VECTSP_7:4; :: thesis: verum

end;

v in {v1} by TARSKI:def 1;
then v in Lin {v1} by VECTSP_7:8;
then A11: v in W1 + (Lin {v1}) by VECTSP_5:2;
A12: not v in Lin {u} by A6, VECTSP10:13;

A13: now :: thesis: not W1 + (Lin {v1}) = W1 + (Lin {u1})

reconsider Wx = the Linear_Compl of U as Subspace of V by VECTSP_4:26;
assume W1 + (Lin {v1}) = W1 + (Lin {u1}) ; :: thesis: contradiction
then consider h, j being Vector of V such that
A14: h in W1 and
A15: j in Lin {u1} and
A16: v1 = h + j by A11, VECTSP_5:1;
consider a being Element of F such that
A17: j = a * u1 by A15, VECTSP10:3;
v1 - (a * u1) = h + ((a * u1) - (a * u1)) by A16, A17, RLVECT_1:def 3;
then v1 - (a * u1) = h + (0. V) by RLVECT_1:15;
then A18: v1 - (a * u1) = h by RLVECT_1:4;
a * u = a * u1 by VECTSP_4:14;
then A19: v1 - (a * u1) = v - (a * u) by VECTSP_4:16;
a * u in Wx by A9, VECTSP_4:21;
then v - (a * u) in Wx by A7, VECTSP_4:23;
then v - (a * u) in the Linear_Compl of U /\ U by A14, A18, A19, VECTSP_5:3;
then v - (a * u) = 0. W2 by A3, VECTSP_4:35;
then h = 0. V by A18, A19, VECTSP_4:11;
then v1 = j by A16, RLVECT_1:4;
hence contradiction by A12, A15, VECTSP10:13; :: thesis: verum

end;

v in W2 ;
then A20: W1 + (Lin {v1}) in pencil (W1,W2,k) by A1, A8, Th15;
u in W2 ;
then W1 + (Lin {u1}) in pencil (W1,W2,k) by A1, A10, Th15;
then 2 c= card (pencil (W1,W2,k)) by A13, A20, PENCIL_1:2;
hence not pencil (W1,W2,k) is trivial by PENCIL_1:4; :: thesis: verum