let F be Field; :: thesis:
let V be finite-dimensional VectSp of F; :: thesis:
let k be Nat; :: thesis:
assume that
A1: 1 <= k and
A2: k < dim V and
A3: 3 <= dim V ; :: thesis:
set S = PencilSpace (V,k);

let B be Block of (PencilSpace (V,k)); :: thesis:
not the topology of (PencilSpace (V,k)) is empty by A1, A2, Th10;
then consider W1, W2 being Subspace of V such that
A4: W1 is Subspace of W2 and
A5: (dim W1) + 1 = k and
A6: dim W2 = k + 1 and
A7: B = pencil (W1,W2,k) by Def4;
A8: the carrier of W1 c= the carrier of V by VECTSP_4:def 2;

per cases by A2, A3, Th1;

suppose k + 1 < dim V ; :: thesis:

then A9: (Omega). W2 <> (Omega). V by A6, VECTSP_9:28;

A10: now :: thesis:

assume A11: the carrier of V = the carrier of W2 ; :: thesis:
(Omega). W2 is Subspace of V by Th4;
hence contradiction by A9, A11, VECTSP_4:29; :: thesis:

end;

the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
then not the carrier of V c= the carrier of W2 by A10;
then consider v being object such that
A12: v in the carrier of V and
A13: not v in the carrier of W2 ;
reconsider v = v as Vector of V by A12;
set X = W1 + (Lin {v});

A14: now :: thesis:

v in {v} by TARSKI:def 1;
then v in Lin {v} by VECTSP_7:8;
then v in W1 + (Lin {v}) by VECTSP_5:2;
then A15: v in the carrier of (W1 + (Lin {v})) ;
assume W1 + (Lin {v}) in B ; :: thesis:
then W1 + (Lin {v}) is Subspace of W2 by A7, Th8;
then the carrier of (W1 + (Lin {v})) c= the carrier of W2 by VECTSP_4:def 2;
hence contradiction by A13, A15; :: thesis:

end;

not v in W2 by A13;
then dim (W1 + (Lin {v})) = k by A4, A5, Th13, VECTSP_4:8;
hence the carrier of (PencilSpace (V,k)) <> B by A14, VECTSP_9:def 2; :: thesis:

end;

suppose A16: ( 2 <= k & k + 1 >= dim V ) ; :: thesis:

set I = the Basis of W1;
reconsider I1 = the Basis of W1 as finite Subset of W1 by VECTSP_9:20;
2 - 1 <= ((dim W1) + 1) - 1 by A5, A16, XREAL_1:9;
then 1 <= card I1 by VECTSP_9:def 1;
then not I1 is empty ;
then consider i being object such that
A17: i in the Basis of W1 ;
reconsider i = i as Vector of W1 by A17;
reconsider J = I1 \ {i} as finite Subset of V by A8, XBOOLE_1:1;
the Basis of W1 is linearly-independent by VECTSP_7:def 3;
then the Basis of W1 \ {i} is linearly-independent by VECTSP_7:1, XBOOLE_1:36;
then reconsider JJ = the Basis of W1 \ {i} as linearly-independent Subset of V by VECTSP_9:11;
J c= the carrier of (Lin J)

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in J ; :: thesis:
then a in Lin J by VECTSP_7:8;
hence a in the carrier of (Lin J) ; :: thesis:

end;

then reconsider JJJ = JJ as linearly-independent Subset of (Lin J) by VECTSP_9:12;
Lin JJJ = Lin J by VECTSP_9:17;
then A18: J is Basis of (Lin J) by VECTSP_7:def 3;
A19: card the Basis of W1 = dim W1 by VECTSP_9:def 1;
set T = the Linear_Compl of W1;
A20: V is_the_direct_sum_of W1, the Linear_Compl of W1 by VECTSP_5:38;
then A21: W1 /\ the Linear_Compl of W1 = (0). V by VECTSP_5:def 4;
k + 1 <= dim V by A2, NAT_1:13;
then dim V = k + 1 by A16, XXREAL_0:1;
then (k + 1) - ((dim W1) + 1) = ((dim W1) + (dim the Linear_Compl of W1)) - ((dim W1) + 1) by A20, VECTSP_9:34;
then consider u, v being Vector of the Linear_Compl of W1 such that
A22: u <> v and
A23: {u,v} is linearly-independent and
A24: (Omega). the Linear_Compl of W1 = Lin {u,v} by A5, VECTSP_9:31;
( the carrier of the Linear_Compl of W1 c= the carrier of V & u in the carrier of the Linear_Compl of W1 ) by VECTSP_4:def 2;
then reconsider u1 = u, v1 = v as Vector of V ;
reconsider Y = {u,v} as linearly-independent Subset of V by A23, VECTSP_9:11;
A25: Y = {u,v} ;
Lin ( the Basis of W1 \ {i}) is Subspace of Lin the Basis of W1 by VECTSP_7:13, XBOOLE_1:36;
then A26: Lin J is Subspace of W1 by VECTSP_9:17;
the carrier of ((Lin J) /\ (Lin {u1,v1})) c= the carrier of ((0). V)

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in the carrier of ((Lin J) /\ (Lin {u1,v1})) ; :: thesis:
then A27: a in (Lin J) /\ (Lin {u1,v1}) ;
then a in Lin {u1,v1} by VECTSP_5:3;
then a in Lin {u,v} by VECTSP_9:17;
then a in the carrier of ModuleStr(# the carrier of the Linear_Compl of W1, the U5 of the Linear_Compl of W1, the ZeroF of the Linear_Compl of W1, the lmult of the Linear_Compl of W1 #) by A24;
then A28: a in the Linear_Compl of W1 ;
a in Lin J by A27, VECTSP_5:3;
then a in W1 by A26, VECTSP_4:8;
then a in W1 /\ the Linear_Compl of W1 by A28, VECTSP_5:3;
hence a in the carrier of ((0). V) by A21; :: thesis:

end;

then A29: ( (0). V is Subspace of (Lin J) /\ (Lin {u1,v1}) & (Lin J) /\ (Lin {u1,v1}) is Subspace of (0). V ) by VECTSP_4:27, VECTSP_4:39;
card J = (card I1) - (card {i}) by A17, EULER_1:4
.= (dim W1) - 1 by A19, CARD_1:30 ;
then dim (Lin J) = (dim W1) - 1 by A18, VECTSP_9:def 1;
then A30: dim ((Lin J) + (Lin {u1,v1})) = ((dim W1) - 1) + 2 by A22, A25, A29, Th14, VECTSP_4:25;
A31: Lin the Basis of W1 = (Omega). W1 by VECTSP_7:def 3;
A32: i in W1 ;

A33: now :: thesis:

reconsider IV = the Basis of W1 as Subset of V by A8, XBOOLE_1:1;
assume A34: i in (Lin J) + (Lin {u1,v1}) ; :: thesis:
IV c= the carrier of ((Lin J) + (Lin {u1,v1}))

let a be object ; :: according to TARSKI:def 3 :: thesis:
{i} c= the Basis of W1 by A17, ZFMISC_1:31;
then A35: ( the Basis of W1 \ {i}) \/ {i} = the Basis of W1 by XBOOLE_1:45;
assume A36: a in IV ; :: thesis:

per cases by A36, A35, XBOOLE_0:def 3;

suppose a in J ; :: thesis:

then A37: a in Lin J by VECTSP_7:8;
then a in V by VECTSP_4:9;
then reconsider o = a as Vector of V ;
o in (Lin J) + (Lin {u1,v1}) by A37, VECTSP_5:2;
hence a in the carrier of ((Lin J) + (Lin {u1,v1})) ; :: thesis:

end;

suppose a in {i} ; :: thesis:

then a = i by TARSKI:def 1;
hence a in the carrier of ((Lin J) + (Lin {u1,v1})) by A34; :: thesis:

end;

end;

end;

then Lin IV is Subspace of (Lin J) + (Lin {u1,v1}) by VECTSP_9:16;
then Lin the Basis of W1 is Subspace of (Lin J) + (Lin {u1,v1}) by VECTSP_9:17;
then A38: W1 is Subspace of (Lin J) + (Lin {u1,v1}) by A31, Th5;
the carrier of (W1 /\ (Lin {u1,v1})) c= the carrier of ((0). V)

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in the carrier of (W1 /\ (Lin {u1,v1})) ; :: thesis:
then A39: a in W1 /\ (Lin {u1,v1}) ;
then a in Lin {u1,v1} by VECTSP_5:3;
then a in Lin {u,v} by VECTSP_9:17;
then a in the carrier of ModuleStr(# the carrier of the Linear_Compl of W1, the U5 of the Linear_Compl of W1, the ZeroF of the Linear_Compl of W1, the lmult of the Linear_Compl of W1 #) by A24;
then A40: a in the Linear_Compl of W1 ;
a in W1 by A39, VECTSP_5:3;
then a in W1 /\ the Linear_Compl of W1 by A40, VECTSP_5:3;
hence a in the carrier of ((0). V) by A21; :: thesis:

end;

then ( (0). V is Subspace of W1 /\ (Lin {u1,v1}) & W1 /\ (Lin {u1,v1}) is Subspace of (0). V ) by VECTSP_4:27, VECTSP_4:39;
then A41: dim (W1 + (Lin {u1,v1})) = (dim W1) + 2 by A22, A25, Th14, VECTSP_4:25;
Lin {u1,v1} is Subspace of (Lin J) + (Lin {u1,v1}) by VECTSP_5:7;
then W1 + (Lin {u1,v1}) is Subspace of (Lin J) + (Lin {u1,v1}) by A38, VECTSP_5:34;
then ((dim W1) + 1) + 1 <= (dim W1) + 1 by A30, A41, VECTSP_9:25;
hence contradiction by NAT_1:13; :: thesis:

end;

assume (Lin J) + (Lin {u1,v1}) in B ; :: thesis:
then W1 is Subspace of (Lin J) + (Lin {u1,v1}) by A7, Th8;
hence contradiction by A32, A33, VECTSP_4:8; :: thesis:

end;

hence the carrier of (PencilSpace (V,k)) <> B by A5, A30, VECTSP_9:def 2; :: thesis:

end;

end;

end;

then the carrier of (PencilSpace (V,k)) is not Block of (PencilSpace (V,k)) ;
hence not PencilSpace (V,k) is degenerated ; :: thesis: