theorem Th31: :: GROUP_3:31

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