consider u being Element of V such that
A1: u <> 0. V by Def8;
thus not Proper_Vectors_of V is empty by A1, Def4; :: thesis: verum