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