let G be addGroup; :: thesis: for A being Subset of G st A <> {} holds
( ([#] the carrier of G) + A = the carrier of G & A + ([#] the carrier of G) = the carrier of G )
let A be Subset of G; :: thesis: ( A <> {} implies ( ([#] the carrier of G) + A = the carrier of G & A + ([#] the carrier of G) = the carrier of G ) )
set y = the Element of A;
assume A1: A <> {} ; :: thesis: ( ([#] the carrier of G) + A = the carrier of G & A + ([#] the carrier of G) = the carrier of G )
then reconsider y = the Element of A as Element of G by Lm1;
thus ([#] the carrier of G) + A = the carrier of G :: thesis: A + ([#] the carrier of G) = the carrier of G

proof

set y = the Element of A;
reconsider y = the Element of A as Element of G by A1, Lm1;
thus ([#] the carrier of G) + A c= the carrier of G ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of G c= ([#] the carrier of G) + A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of G or x in ([#] the carrier of G) + A )
assume x in the carrier of G ; :: thesis: x in ([#] the carrier of G) + A
then reconsider a = x as Element of G ;
(a + (- y)) + y = a + ((- y) + y) by RLVECT_1:def 3
.= a + (0_ G) by Def5
.= a by Def4 ;
hence x in ([#] the carrier of G) + A by A1; :: thesis: verum

end;

thus A + ([#] the carrier of G) c= the carrier of G ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of G c= A + ([#] the carrier of G)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of G or x in A + ([#] the carrier of G) )
assume x in the carrier of G ; :: thesis: x in A + ([#] the carrier of G)
then reconsider a = x as Element of G ;
y + ((- y) + a) = (y + (- y)) + a by RLVECT_1:def 3
.= (0_ G) + a by Def5
.= a by Def4 ;
hence x in A + ([#] the carrier of G) by A1; :: thesis: verum