let G be Group; :: thesis: for x, y, z being Element of G
for A being Subset of G holds
( z in (x * A) * y iff ex a being Element of G st
( z = (x * a) * y & a in A ) )
let x, y, z be Element of G; :: thesis: for A being Subset of G holds
( z in (x * A) * y iff ex a being Element of G st
( z = (x * a) * y & a in A ) )
let A be Subset of G; :: thesis: ( z in (x * A) * y iff ex a being Element of G st
( z = (x * a) * y & a in A ) )
thus ( z in (x * A) * y implies ex a being Element of G st
( z = (x * a) * y & a in A ) ) :: thesis: ( ex a being Element of G st
( z = (x * a) * y & a in A ) implies z in (x * A) * y )

proof

assume z in (x * A) * y ; :: thesis: ex a being Element of G st
( z = (x * a) * y & a in A )
then consider b being Element of G such that
A1: ( z = b * y & b in x * A ) by GROUP_2:34;
consider u being Element of G such that
A2: ( b = x * u & u in A ) by A1, GROUP_2:33;
take a = u; :: thesis: ( z = (x * a) * y & a in A )
thus ( z = (x * a) * y & a in A ) by A1, A2; :: thesis: verum

end;

given a being Element of G such that A3: ( z = (x * a) * y & a in A ) ; :: thesis: z in (x * A) * y
ex h being Element of G st
( z = h * y & h in x * A )

proof

take h = x * a; :: thesis: ( z = h * y & h in x * A )
thus ( z = h * y & h in x * A ) by A3, GROUP_2:33; :: thesis: verum

end;

hence z in (x * A) * y by GROUP_2:34; :: thesis: verum