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 that
A2: v = y and
A3: W = X ; :: thesis: X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
Lin {v} = Lin {y} by A2, Th13;
hence ModuleStr(# the carrier of (X + (Lin {v})), the addF of (X + (Lin {v})), the ZeroF of (X + (Lin {v})), the lmult of (X + (Lin {v})) #) = W + (Lin {y}) by A3, Th12; :: 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
A4: ( ( 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:30;

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 A4;

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

z in Lin {y} by A5, VECTSP_5:3;
then consider a being Element of K such that
A7: z = a * y by Th3;
A8: z in W by A5, VECTSP_5:3;

now :: thesis: contradiction

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:15;
hence contradiction by A6, VECTSP_4:17; :: thesis: verum

end;

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

y = (1_ K) * y
.= ((a ") * a) * y by A9, VECTSP_1:def 10
.= (a ") * (a * y) by VECTSP_1:def 16 ;
hence contradiction by A1, A2, A3, A8, A7, VECTSP_4:21; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

z = 0. (X + (Lin {v})) by A11, VECTSP_4:35;
hence contradiction by A10, VECTSP_4:17; :: thesis: verum

end;

end;