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;
consider x being Element of A;
A6: not K is trivial by A1, LMOD_6:6;
reconsider a = x 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:37;
then A7: A = A1 \/ (A \ A1) by XBOOLE_1:45;
A1 misses A \ A1 by XBOOLE_1:79;
then A8: V is_the_direct_sum_of Lin A1, Lin (A \ A1) by A3, A7, Th6;
A9: 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 A4, A5, A6, A8, Th1, LMOD_6:def 6; :: 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 A9; :: thesis: verum