let V be non empty Abelian right_zeroed addLoopStr ; :: thesis: for A being Subset of V holds (0. V) + A = A

let A be Subset of V; :: thesis: (0. V) + A = A

thus (0. V) + A c= A :: according to XBOOLE_0:def 10 :: thesis: A c= (0. V) + A

assume A1: x in A ; :: thesis: x in (0. V) + A

then reconsider v = x as Element of V ;

(0. V) + v = v by RLVECT_1:def 4;

hence x in (0. V) + A by A1; :: thesis: verum

let A be Subset of V; :: thesis: (0. V) + A = A

thus (0. V) + A c= A :: according to XBOOLE_0:def 10 :: thesis: A c= (0. V) + A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in (0. V) + A )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (0. V) + A or x in A )

assume x in (0. V) + A ; :: thesis: x in A

then ex s being Element of V st

( x = (0. V) + s & s in A ) ;

hence x in A by RLVECT_1:def 4; :: thesis: verum

end;assume x in (0. V) + A ; :: thesis: x in A

then ex s being Element of V st

( x = (0. V) + s & s in A ) ;

hence x in A by RLVECT_1:def 4; :: thesis: verum

assume A1: x in A ; :: thesis: x in (0. V) + A

then reconsider v = x as Element of V ;

(0. V) + v = v by RLVECT_1:def 4;

hence x in (0. V) + A by A1; :: thesis: verum