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 9;
then consider u, v being Element of V such that
A1: ( x = u + v & u in M ) and
A2: v in {(0. V)} ;
v = 0. V by A2, TARSKI:def 1;
hence x in M by A1, RLVECT_1:def 4; :: thesis: verum

end;

then A3: M + {(0. V)} c= M ;
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)} )
A4: ( x = x + (0. V) & 0. V in {(0. V)} ) by RLVECT_1:def 4, TARSKI:def 1;
assume x in M ; :: thesis: x in M + {(0. V)}
then x in { (u + v) where u, v is Element of V : ( u in M & v in {(0. V)} ) } by A4;
hence x in M + {(0. V)} by RUSUB_4:def 9; :: thesis: verum

end;

then M c= M + {(0. V)} ;
hence M + {(0. V)} = M by A3; :: thesis: verum