theorem Th7: :: GROUP_5:7

for x being set
for G being Group
for N1, N2 being strict normal Subgroup of G holds
( x in N1 "\/" N2 iff ex a, b being Element of G st
( x = a * b & a in N1 & b in N2 ) )