let V be RealLinearSpace; :: 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 Th23;
hence RLSStruct(# the carrier of (X + (Lin {v})),the U2 of (X + (Lin {v})),the addF of (X + (Lin {v})),the Mult of (X + (Lin {v})) #) = W + (Lin {y}) by A2, Th22; :: according to RLSUB_2: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 RLSUB_1:39;

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, RLSUB_2:7;
z in Lin {y} by A4, RLSUB_2:7;
then consider a being Real such that
A7: z = a * y by RLVECT_4:11;

now

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

suppose a = 0 ; :: thesis: contradiction

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

end;

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

y = 1 * y by RLVECT_1:def 9
.= ((a " ) * a) * y by A8, XCMPLX_0:def 7
.= (a " ) * (a * y) by RLVECT_1:def 9 ;
hence contradiction by A1, A2, A6, A7, RLSUB_1: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, RLVECT_3:36;
hence contradiction by A9, RLSUB_1:25; :: thesis: verum

end;

end;