set x = the Element of V1;
reconsider x1 = the Element of V1 as Element of V by A1, TARSKI:def 3;
( - x1 in V1 & x1 + (- x1) = 0. V ) by A1, RLVECT_1:def 10;
hence 0. V is Element of V1 by A1, IDEAL_1:def 1; :: thesis: verum