consider A being Subset of V such that

A3: A is base by A2, VECTSP_7:def 4;

reconsider A = A as Subset of V ;

A4: A is linearly-independent by A3, VECTSP_7:def 3;

A5: A <> {} by A1, A3, Th4;

set x = the Element of A;

reconsider a = the Element of A as Vector of V by A5, TARSKI:def 3;

reconsider A1 = {a} as Subset of V ;

set A2 = A \ A1;

set H = Lin (A \ A1);

A1 c= A by A5, ZFMISC_1:31;

then A6: A = A1 \/ (A \ A1) by XBOOLE_1:45;

A1 misses A \ A1 by XBOOLE_1:79;

then A7: V is_the_direct_sum_of Lin A1, Lin (A \ A1) by A3, A6, Th6;

A8: ex a being Vector of V st

( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) )

( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) )

thus ex a being Vector of V st

( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) ) by A8; :: thesis: verum

A3: A is base by A2, VECTSP_7:def 4;

reconsider A = A as Subset of V ;

A4: A is linearly-independent by A3, VECTSP_7:def 3;

A5: A <> {} by A1, A3, Th4;

set x = the Element of A;

reconsider a = the Element of A as Vector of V by A5, TARSKI:def 3;

reconsider A1 = {a} as Subset of V ;

set A2 = A \ A1;

set H = Lin (A \ A1);

A1 c= A by A5, ZFMISC_1:31;

then A6: A = A1 \/ (A \ A1) by XBOOLE_1:45;

A1 misses A \ A1 by XBOOLE_1:79;

then A7: V is_the_direct_sum_of Lin A1, Lin (A \ A1) by A3, A6, Th6;

A8: ex a being Vector of V st

( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) )

proof

take
Lin (A \ A1)
; :: thesis: ex a being Vector of V st
take
a
; :: thesis: ( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) )

thus ( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) ) by A1, A4, A5, A7, Th1, LMOD_6:6, LMOD_6:def 4; :: thesis: verum

end;thus ( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) ) by A1, A4, A5, A7, Th1, LMOD_6:6, LMOD_6:def 4; :: thesis: verum

( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) )

thus ex a being Vector of V st

( a <> 0. V & V is_the_direct_sum_of <:a:>, Lin (A \ A1) ) by A8; :: thesis: verum