let V be non empty right_zeroed addLoopStr ; :: thesis: for M being Subset of V holds M + {(0. V)} = M
let M be Subset of V; :: thesis: M + {(0. V)} = M
for x being Element of V st x in M + {(0. V)} holds
x in M

proof

let x be Element of V; :: thesis: ( x in M + {(0. V)} implies x in M )
assume x in M + {(0. V)} ; :: thesis: x in M
then x in { (u + v) where u, v is Element of V : ( u in M & v in {(0. V)} ) } by RUSUB_4:def 10;
then consider u, v being Element of V such that
A1: ( x = u + v & u in M & v in {(0. V)} ) ;
v = 0. V by A1, TARSKI:def 1;
hence x in M by A1, RLVECT_1:def 7; :: thesis: verum

end;

then A2: M + {(0. V)} c= M by SUBSET_1:7;
for x being Element of V st x in M holds
x in M + {(0. V)}

proof

let x be Element of V; :: thesis: ( x in M implies x in M + {(0. V)} )
assume A3: x in M ; :: thesis: x in M + {(0. V)}
A4: x = x + (0. V) by RLVECT_1:def 7;
0. V in {(0. V)} by TARSKI:def 1;
then x in { (u + v) where u, v is Element of V : ( u in M & v in {(0. V)} ) } by A3, A4;
hence x in M + {(0. V)} by RUSUB_4:def 10; :: thesis: verum

end;

then M c= M + {(0. V)} by SUBSET_1:7;
hence M + {(0. V)} = M by A2, XBOOLE_0:def 10; :: thesis: verum