ex u being Element of V st u <> 0. V by Def19;
hence not NonZero V is empty by ZFMISC_1:64; :: thesis: verum