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