theorem Th8: :: GROUP_2:8

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