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

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

( ([#] 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

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)
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;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

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