theorem Th31: :: GROUP_1A:232

for x being set
for G being addGroup
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 ) ) ;