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

for x being Element of V st x in M holds

x in M + {(0. V)}

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

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

then A3:
M + {(0. V)} c= M
;
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;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

for x being Element of V st x in M holds

x in M + {(0. V)}

proof

then
M c= M + {(0. V)}
;
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;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

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