consider x being Linear_Combination of V;
x in LinComb V by Def16;
hence not LinComb V is empty ; :: thesis: verum