set x = the Linear_Combination of V;
the Linear_Combination of V in LinComb V by Def14;
hence not LinComb V is empty ; :: thesis: verum