for x being object
for G being addGroup
for A being Subset of G
for H being Subgroup of G holds
( x in A + H iff ex g1, g2 being Element of G st
( x = g1 + g2 & g1 in A & g2 in H ) )