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 1 <= k & k < dim V & (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 1 <= k & k < dim V & (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 1 <= k & k < dim V & (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil W1,W2,k is trivial )
assume A1: W1 is Subspace of W2 ; :: thesis: for k being Nat st 1 <= k & k < dim V & (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil W1,W2,k is trivial
let k be Nat; :: thesis: ( 1 <= k & k < dim V & (dim W1) + 1 = k & dim W2 = k + 1 implies not pencil W1,W2,k is trivial )
assume A2: ( 1 <= k & k < dim V & (dim W1) + 1 = k & dim W2 = k + 1 ) ; :: thesis: not pencil W1,W2,k is trivial
reconsider U = W1 as Subspace of W2 by A1;
consider W being Linear_Compl of U;
A3: W2 is_the_direct_sum_of W,U by VECTSP_5:def 5;
then dim W2 = (dim U) + (dim W) by VECTSP_9:38;
then consider u, v being Vector of W such that
A4: ( u <> v & {u,v} is linearly-independent & (Omega). W = Lin {u,v} ) by A2, VECTSP_9:35;

A5: now

assume v in Lin {u} ; :: thesis: contradiction
then consider a being Element of F such that
A6: v = a * u by VECTSP10:4;
thus contradiction by A4, A6, VECTSP_7:8; :: thesis: verum

end;

A7: ( VectSpStr(# the carrier of W2,the U5 of W2,the U2 of W2,the lmult of W2 #) = W + U & W /\ U = (0). W2 ) by A3, VECTSP_5:def 4;
reconsider u = u, v = v as Vector of W2 by VECTSP_4:18;
A8: u in W by STRUCT_0:def 5;
A9: u in W2 by STRUCT_0:def 5;

A10: now

assume u in W1 ; :: thesis: contradiction
then u in (0). W2 by A7, A8, VECTSP_5:7;
then u = 0. W2 by VECTSP_4:46;
then u = 0. W by VECTSP_4:19;
hence contradiction by A4, VECTSP_7:6; :: thesis: verum

end;

A11: v in W by STRUCT_0:def 5;
A12: v in W2 by STRUCT_0:def 5;

A13: now

assume v in W1 ; :: thesis: contradiction
then v in (0). W2 by A7, A11, VECTSP_5:7;
then v = 0. W2 by VECTSP_4:46;
then v = 0. W by VECTSP_4:19;
hence contradiction by A4, VECTSP_7:6; :: thesis: verum

end;

reconsider u1 = u, v1 = v as Vector of V by VECTSP_4:18;
v in {v1} by TARSKI:def 1;
then v in Lin {v1} by VECTSP_7:13;
then A14: v in W1 + (Lin {v1}) by VECTSP_5:6;
A15: not v in Lin {u} by A5, VECTSP10:14;

A16: now

assume W1 + (Lin {v1}) = W1 + (Lin {u1}) ; :: thesis: contradiction
then consider h, j being Vector of V such that
A17: ( h in W1 & j in Lin {u1} & v1 = h + j ) by A14, VECTSP_5:5;
consider a being Element of F such that
A18: j = a * u1 by A17, VECTSP10:4;
v1 - (a * u1) = h + ((a * u1) - (a * u1)) by A17, A18, RLVECT_1:def 6;
then v1 - (a * u1) = h + (0. V) by RLVECT_1:28;
then A19: v1 - (a * u1) = h by RLVECT_1:10;
reconsider Wx = W as Subspace of V by VECTSP_4:34;
a * u in Wx by A8, VECTSP_4:29;
then A20: v - (a * u) in Wx by A11, VECTSP_4:31;
a * u = a * u1 by VECTSP_4:22;
then A21: v1 - (a * u1) = v - (a * u) by VECTSP_4:24;
then v - (a * u) in W /\ U by A17, A19, A20, VECTSP_5:7;
then v - (a * u) = 0. W2 by A7, VECTSP_4:46;
then h = 0. V by A19, A21, VECTSP_4:19;
then v1 = j by A17, RLVECT_1:10;
hence contradiction by A15, A17, VECTSP10:14; :: thesis: verum

end;

( W1 + (Lin {u1}) in pencil W1,W2,k & W1 + (Lin {v1}) in pencil W1,W2,k ) by A2, A9, A10, A12, A13, Th16;
then 2 c= card (pencil W1,W2,k) by A16, PENCIL_1:2;
hence not pencil W1,W2,k is trivial by PENCIL_1:4; :: thesis: verum