let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for M, N being Subset of V
for v being Element of V holds
( M = N + {v} iff M - {v} = N )
let M, N be Subset of V; :: thesis: for v being Element of V holds
( M = N + {v} iff M - {v} = N )
let v be Element of V; :: thesis: ( M = N + {v} iff M - {v} = N )
A1: ( M - {v} = N implies M = N + {v} )

proof

assume A2: M - {v} = N ; :: thesis: M = N + {v}
for x being object st x in N + {v} holds
x in M

proof

let x be object ; :: thesis: ( x in N + {v} implies x in M )
assume A3: x in N + {v} ; :: thesis: x in M
then reconsider x = x as Element of V ;
x in { (u1 + v1) where u1, v1 is Element of V : ( u1 in N & v1 in {v} ) } by A3, RUSUB_4:def 9;
then consider u1, v1 being Element of V such that
A4: x = u1 + v1 and
A5: u1 in N and
A6: v1 in {v} ;
A7: x - v1 = u1 + (v1 - v1) by A4, RLVECT_1:def 3
.= u1 + (0. V) by RLVECT_1:15
.= u1 ;
v1 = v by A6, TARSKI:def 1;
then consider u2, v2 being Element of V such that
A8: x - v = u2 - v2 and
A9: u2 in M and
A10: v2 in {v} by A2, A5, A7;
v2 = v by A10, TARSKI:def 1;
then (x - v) + v = u2 - (v - v) by A8, RLVECT_1:29
.= u2 - (0. V) by RLVECT_1:15
.= u2 ;
then u2 = x - (v - v) by RLVECT_1:29
.= x - (0. V) by RLVECT_1:15 ;
hence x in M by A9; :: thesis: verum

end;

then A11: N + {v} c= M ;
for x being object st x in M holds
x in N + {v}

proof

let x be object ; :: thesis: ( x in M implies x in N + {v} )
assume A12: x in M ; :: thesis: x in N + {v}
then reconsider x = x as Element of V ;
A13: v in {v} by TARSKI:def 1;
then x - v in { (u2 - v2) where u2, v2 is Element of V : ( u2 in M & v2 in {v} ) } by A12;
then consider u2 being Element of V such that
A14: x - v = u2 and
A15: u2 in N by A2;
u2 + v = x - (v - v) by A14, RLVECT_1:29
.= x - (0. V) by RLVECT_1:15
.= x ;
then x in { (u1 + v1) where u1, v1 is Element of V : ( u1 in N & v1 in {v} ) } by A13, A15;
hence x in N + {v} by RUSUB_4:def 9; :: thesis: verum

end;

then M c= N + {v} ;
hence M = N + {v} by A11; :: thesis: verum

end;

( M = N + {v} implies M - {v} = N )

proof

assume A16: M = N + {v} ; :: thesis: M - {v} = N
for x being object st x in M - {v} holds
x in N

proof

let x be object ; :: thesis: ( x in M - {v} implies x in N )
assume A17: x in M - {v} ; :: thesis: x in N
then reconsider x = x as Element of V ;
consider u1, v1 being Element of V such that
A18: x = u1 - v1 and
A19: u1 in M and
A20: v1 in {v} by A17;
A21: x + v1 = u1 - (v1 - v1) by A18, RLVECT_1:29
.= u1 - (0. V) by RLVECT_1:15
.= u1 ;
v1 = v by A20, TARSKI:def 1;
then x + v in { (u2 + v2) where u2, v2 is Element of V : ( u2 in N & v2 in {v} ) } by A16, A19, A21, RUSUB_4:def 9;
then consider u2, v2 being Element of V such that
A22: ( x + v = u2 + v2 & u2 in N ) and
A23: v2 in {v} ;
v2 = v by A23, TARSKI:def 1;
hence x in N by A22, RLVECT_1:8; :: thesis: verum

end;

then A24: M - {v} c= N ;
for x being object st x in N holds
x in M - {v}

proof

let x be object ; :: thesis: ( x in N implies x in M - {v} )
assume A25: x in N ; :: thesis: x in M - {v}
then reconsider x = x as Element of V ;
A26: v in {v} by TARSKI:def 1;
then x + v in { (u2 + v2) where u2, v2 is Element of V : ( u2 in N & v2 in {v} ) } by A25;
then x + v in M by A16, RUSUB_4:def 9;
then consider u2 being Element of V such that
A27: x + v = u2 and
A28: u2 in M ;
u2 - v = x + (v - v) by A27, RLVECT_1:def 3
.= x + (0. V) by RLVECT_1:15
.= x ;
hence x in M - {v} by A26, A28; :: thesis: verum

end;

then N c= M - {v} ;
hence M - {v} = N by A24; :: thesis: verum

end;

hence ( M = N + {v} iff M - {v} = N ) by A1; :: thesis: verum