let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for W1, W2, P, Q being Subspace of V
for k being Nat st 1 <= k & k < dim V & (dim W1) + 1 = k & dim W2 = k + 1 & P in pencil W1,W2,k & Q in pencil W1,W2,k & P <> Q holds
( P /\ Q = (Omega). W1 & P + Q = (Omega). W2 )
let V be finite-dimensional VectSp of F; :: thesis: for W1, W2, P, Q being Subspace of V
for k being Nat st 1 <= k & k < dim V & (dim W1) + 1 = k & dim W2 = k + 1 & P in pencil W1,W2,k & Q in pencil W1,W2,k & P <> Q holds
( P /\ Q = (Omega). W1 & P + Q = (Omega). W2 )
let W1, W2, P0, Q0 be Subspace of V; :: thesis: for k being Nat st 1 <= k & k < dim V & (dim W1) + 1 = k & dim W2 = k + 1 & P0 in pencil W1,W2,k & Q0 in pencil W1,W2,k & P0 <> Q0 holds
( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 )
let k be Nat; :: thesis: ( 1 <= k & k < dim V & (dim W1) + 1 = k & dim W2 = k + 1 & P0 in pencil W1,W2,k & Q0 in pencil W1,W2,k & P0 <> Q0 implies ( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 ) )
assume A1: ( 1 <= k & k < dim V & (dim W1) + 1 = k & dim W2 = k + 1 & P0 in pencil W1,W2,k & Q0 in pencil W1,W2,k & P0 <> Q0 ) ; :: thesis: ( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 )
consider P being strict Subspace of V such that
A2: ( P = P0 & dim P = k ) by A1, VECTSP_9:def 3;
consider Q being strict Subspace of V such that
A3: ( Q = Q0 & dim Q = k ) by A1, VECTSP_9:def 3;
P /\ Q is Subspace of P by VECTSP_5:20;
then A4: dim (P /\ Q) <= k by A2, VECTSP_9:29;
( W1 is Subspace of P & W1 is Subspace of Q ) by A1, A2, A3, Th9;
then A5: W1 is Subspace of P /\ Q by VECTSP_5:24;

per cases ( dim W1 = dim (P /\ Q) or dim (P /\ Q) = k ) by A1, A4, A5, NAT_1:9, VECTSP_9:29;

suppose A6: dim W1 = dim (P /\ Q) ; :: thesis: ( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 )

then (Omega). W1 = (Omega). (P /\ Q) by A5, VECTSP_9:32;
hence P0 /\ Q0 = (Omega). W1 by A2, A3; :: thesis: P0 + Q0 = (Omega). W2
( P is Subspace of W2 & Q is Subspace of W2 ) by A1, A2, A3, Th9;
then A7: P + Q is Subspace of W2 by VECTSP_5:40;
((dim (P + Q)) + (dim W1)) - (dim W1) = ((dim P) + (dim Q)) - (dim W1) by A6, VECTSP_9:36;
then (Omega). W2 = (Omega). (P + Q) by A1, A2, A3, A7, VECTSP_9:32;
hence P0 + Q0 = (Omega). W2 by A2, A3; :: thesis: verum

end;

suppose A8: dim (P /\ Q) = k ; :: thesis: ( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 )

P /\ Q is Subspace of P by VECTSP_5:20;
then A9: (Omega). (P /\ Q) = (Omega). P by A2, A8, VECTSP_9:32;
P /\ Q is Subspace of Q by VECTSP_5:20;
then (Omega). (P /\ Q) = (Omega). Q by A3, A8, VECTSP_9:32;
hence ( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 ) by A1, A2, A3, A9; :: thesis: verum

end;

end;