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 ; :: 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 ;
consider c, d being Element of G such that
A7: ( y = c * d & c in N1 & d in N2 ) by ;
A8: x * y = ((a * b) * c) * d by
.= (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
.= (a * b9) * (c9 * d) by GROUP_1:def 3 ;
A11: a * b9 in N1 by ;
c9 * d in N2 by ;
hence x * y in N1 * N2 by ; :: 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 ;
( b " in N2 & a " in N1 ) by ;
then x " in N2 * N1 by ;
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 ; :: thesis: verum