consider x being C_Linear_Combination of V;
x in C_LinComb V by Def8;
hence not C_LinComb V is empty ; :: thesis: verum