for G being Group
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 ) )