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 ) )
assume A1: A <> {} ; :: thesis: ( ([#] the carrier of G) * A = the carrier of G & A * ([#] the carrier of G) = the carrier of G )
thus ([#] the carrier of G) * A = the carrier of G :: thesis: A * ([#] the carrier of G) = the carrier of G

proof

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 set ; :: 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 ;
consider y being Element of A;
reconsider y = y as Element of G by A1, Lm1;
(a * (y " )) * y = a * ((y " ) * y) by GROUP_1:def 4
.= a * (1_ G) by GROUP_1:def 6
.= a by GROUP_1:def 5 ;
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 set ; :: 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 ;
consider y being Element of A;
reconsider y = y as Element of G by A1, Lm1;
y * ((y " ) * a) = (y * (y " )) * a by GROUP_1:def 4
.= (1_ G) * a by GROUP_1:def 6
.= a by GROUP_1:def 5 ;
hence x in A * ([#] the carrier of G) by A1; :: thesis: verum