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 (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 (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 (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: ( (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 that
A1: (dim W1) + 1 = k and
A2: dim W2 = k + 1 and
A3: P0 in pencil (W1,W2,k) and
A4: Q0 in pencil (W1,W2,k) and
A5: P0 <> Q0 ; :: thesis: ( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 )
consider Q being strict Subspace of V such that
A6: Q = Q0 and
A7: dim Q = k by A4, VECTSP_9:def 2;
A8: W1 is Subspace of Q by A4, A6, Th8;
consider P being strict Subspace of V such that
A9: P = P0 and
A10: dim P = k by A3, VECTSP_9:def 2;
W1 is Subspace of P by A3, A9, Th8;
then A11: W1 is Subspace of P /\ Q by A8, VECTSP_5:19;
P /\ Q is Subspace of P by VECTSP_5:15;
then A12: dim (P /\ Q) <= k by A10, VECTSP_9:25;

per cases ( dim W1 = dim (P /\ Q) or dim (P /\ Q) = k ) by A1, A12, A11, NAT_1:9, VECTSP_9:25;

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

then (Omega). W1 = (Omega). (P /\ Q) by A11, VECTSP_9:28;
hence P0 /\ Q0 = (Omega). W1 by A9, A6; :: thesis: P0 + Q0 = (Omega). W2
( P is Subspace of W2 & Q is Subspace of W2 ) by A3, A4, A9, A6, Th8;
then A14: P + Q is Subspace of W2 by VECTSP_5:34;
((dim (P + Q)) + (dim W1)) - (dim W1) = ((dim P) + (dim Q)) - (dim W1) by A13, VECTSP_9:32;
then (Omega). W2 = (Omega). (P + Q) by A1, A2, A10, A7, A14, VECTSP_9:28;
hence P0 + Q0 = (Omega). W2 by A9, A6; :: thesis: verum

end;

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

P /\ Q is Subspace of Q by VECTSP_5:15;
then A16: (Omega). (P /\ Q) = (Omega). Q by A7, A15, VECTSP_9:28;
P /\ Q is Subspace of P by VECTSP_5:15;
then (Omega). (P /\ Q) = (Omega). P by A10, A15, VECTSP_9:28;
hence ( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 ) by A5, A9, A6, A16; :: thesis: verum

end;

end;