theorem Th9: :: GROUP_11:9

for G being Group
for N, N1, N2 being Subgroup of G st the carrier of N = N1 * N2 holds
( N1 is Subgroup of N & N2 is Subgroup of N )