let K be Field; :: thesis: for V being VectSp of K
for v being Vector of V
for X being Subspace of V st not v in X holds
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let V be VectSp of K; :: thesis: for v being Vector of V
for X being Subspace of V st not v in X holds
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let v be Vector of V; :: thesis: for X being Subspace of V st not v in X holds
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let X be Subspace of V; :: thesis: ( not v in X implies for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y} )
assume A1: not v in X ; :: thesis: for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let y be Vector of (X + (Lin {v})); :: thesis: for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let W be Subspace of X + (Lin {v}); :: thesis: ( v = y & W = X implies X + (Lin {v}) is_the_direct_sum_of W, Lin {y} )
assume A2: ( v = y & W = X ) ; :: thesis: X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
then Lin {v} = Lin {y} by Th14;
hence VectSpStr(# the carrier of (X + (Lin {v})),the addF of (X + (Lin {v})),the U2 of (X + (Lin {v})),the lmult of (X + (Lin {v})) #) = W + (Lin {y}) by A2, Th13; :: according to VECTSP_5:def 4 :: thesis: W /\ (Lin {y}) = (0). (X + (Lin {v}))
assume W /\ (Lin {y}) <> (0). (X + (Lin {v})) ; :: thesis: contradiction
then consider z being Vector of (X + (Lin {v})) such that
A3: ( ( z in W /\ (Lin {y}) & not z in (0). (X + (Lin {v})) ) or ( z in (0). (X + (Lin {v})) & not z in W /\ (Lin {y}) ) ) by VECTSP_4:38;

per cases ( ( z in W /\ (Lin {y}) & not z in (0). (X + (Lin {v})) ) or ( not z in W /\ (Lin {y}) & z in (0). (X + (Lin {v})) ) ) by A3;

suppose that A4: z in W /\ (Lin {y}) and
A5: not z in (0). (X + (Lin {v})) ; :: thesis: contradiction

A6: z in W by A4, VECTSP_5:7;
z in Lin {y} by A4, VECTSP_5:7;
then consider a being Element of K such that
A7: z = a * y by Th4;

now

per cases ( a = 0. K or a <> 0. K ) ;

suppose a = 0. K ; :: thesis: contradiction

then z = 0. (X + (Lin {v})) by A7, VECTSP_1:60;
hence contradiction by A5, VECTSP_4:25; :: thesis: verum

end;

suppose A8: a <> 0. K ; :: thesis: contradiction

y = (1_ K) * y by VECTSP_1:def 26
.= ((a " ) * a) * y by A8, VECTSP_1:def 22
.= (a " ) * (a * y) by VECTSP_1:def 26 ;
hence contradiction by A1, A2, A6, A7, VECTSP_4:29; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose that A9: not z in W /\ (Lin {y}) and
A10: z in (0). (X + (Lin {v})) ; :: thesis: contradiction

z = 0. (X + (Lin {v})) by A10, VECTSP_4:46;
hence contradiction by A9, VECTSP_4:25; :: thesis: verum

end;

end;