set x = the C_Linear_Combination of V;
the C_Linear_Combination of V in C_LinComb V by Def12;
hence not C_LinComb V is empty ; :: thesis: verum