theorem Th28: :: GROUP_2:28

for x being object
for G being non empty multMagma
for A being Subset of G
for g being Element of G holds
( x in A * g iff ex h being Element of G st
( x = h * g & h in A ) )