let G be Group; :: 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 GROUP_1:def 3
.= a * (1_ G) by GROUP_1:def 5
.= a by GROUP_1:def 4 ;
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 GROUP_1:def 3
.= (1_ G) * a by GROUP_1:def 5
.= a by GROUP_1:def 4 ;
hence x in A * ([#] the carrier of G) by A1; :: thesis: verum