consider A being Subset of V such that
A3: A is base by A2, MOD_3:def 3;
reconsider A = A as Subset of V ;
A4: A is linearly-independent by A3, MOD_3:def 2;
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 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;

take Lin (A \ A1) ; :: thesis: ex a being Vector of V st
( 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