let G be Group; :: thesis: for N1, N2 being strict normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N1 * N2
let N1, N2 be strict normal Subgroup of G; :: thesis: ex M being strict normal Subgroup of G st the carrier of M = N1 * N2
consider M being strict Subgroup of G such that
A1: the carrier of M = N1 * N2 by Th7;
for x, y being Element of G st y in M holds
(x * y) * (x ") in M
proof
let x, y be Element of G; :: thesis: ( y in M implies (x * y) * (x ") in M )
assume y in M ; :: thesis: (x * y) * (x ") in M
then y in the carrier of M by STRUCT_0:def 5;
then consider a, b being Element of G such that
A2: ( y = a * b & a in N1 & b in N2 ) by A1, Th6;
A3: (x * y) * (x ") = ((x * a) * b) * (x ") by A2, GROUP_1:def 3
.= (x * a) * (b * (x ")) by GROUP_1:def 3
.= ((x * a) * (1_ G)) * (b * (x ")) by GROUP_1:def 4
.= ((x * a) * ((x ") * x)) * (b * (x ")) by GROUP_1:def 5
.= (((x * a) * (x ")) * x) * (b * (x ")) by GROUP_1:def 3
.= ((x * a) * (x ")) * (x * (b * (x "))) by GROUP_1:def 3
.= ((x * a) * (x ")) * ((x * b) * (x ")) by GROUP_1:def 3 ;
( (x * a) * (x ") in N1 & (x * b) * (x ") in N2 ) by A2, Th4;
then (x * y) * (x ") in N1 * N2 by A3, Th6;
hence (x * y) * (x ") in M by A1, STRUCT_0:def 5; :: thesis: verum
end;
then M is normal Subgroup of G by Th5;
hence ex M being strict normal Subgroup of G st the carrier of M = N1 * N2 by A1; :: thesis: verum