let G be Group; :: thesis: for N1, N2 being strict normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N1 * N2
let N1, N2 be strict normal Subgroup of G; :: thesis: ex M being strict Subgroup of G st the carrier of M = N1 * N2
A1: 1_ G in N1 * N2

proof

A2: ( 1_ G in N1 & 1_ G in N2 ) by GROUP_2:46;
(1_ G) * (1_ G) = 1_ G by GROUP_1:def 4;
hence 1_ G in N1 * N2 by A2, Th6; :: thesis: verum

end;

A3: for x, y being Element of G st x in N1 * N2 & y in N1 * N2 holds
x * y in N1 * N2

proof

let x, y be Element of G; :: thesis: ( x in N1 * N2 & y in N1 * N2 implies x * y in N1 * N2 )
assume that
A4: x in N1 * N2 and
A5: y in N1 * N2 ; :: thesis: x * y in N1 * N2
consider a, b being Element of G such that
A6: ( x = a * b & a in N1 & b in N2 ) by A4, Th6;
consider c, d being Element of G such that
A7: ( y = c * d & c in N1 & d in N2 ) by A5, Th6;
A8: x * y = ((a * b) * c) * d by A6, A7, GROUP_1:def 3
.= (a * (b * c)) * d by GROUP_1:def 3 ;
b * c in N2 * N1 by A6, A7, Th6;
then b * c in N1 * N2 by GROUP_3:125;
then consider b9, c9 being Element of G such that
A9: ( b * c = b9 * c9 & b9 in N1 & c9 in N2 ) by Th6;
A10: x * y = ((a * b9) * c9) * d by A8, A9, GROUP_1:def 3
.= (a * b9) * (c9 * d) by GROUP_1:def 3 ;
A11: a * b9 in N1 by A6, A9, GROUP_2:50;
c9 * d in N2 by A7, A9, GROUP_2:50;
hence x * y in N1 * N2 by A10, A11, Th6; :: thesis: verum

end;

for x being Element of G st x in N1 * N2 holds
x " in N1 * N2

proof

let x be Element of G; :: thesis: ( x in N1 * N2 implies x " in N1 * N2 )
assume x in N1 * N2 ; :: thesis: x " in N1 * N2
then consider a, b being Element of G such that
A12: ( x = a * b & a in N1 & b in N2 ) by Th6;
A13: x " = (b ") * (a ") by A12, GROUP_1:17;
( b " in N2 & a " in N1 ) by A12, GROUP_2:51;
then x " in N2 * N1 by A13, Th6;
hence x " in N1 * N2 by GROUP_3:125; :: thesis: verum

end;

hence ex M being strict Subgroup of G st the carrier of M = N1 * N2 by A1, A3, GROUP_2:52; :: thesis: verum