v1 = 0. V by STRUCT_0:def 12;
hence v2 + v1 = v2 by Th4; :: thesis: verum