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

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

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

then
M is normal Subgroup of G
by Th5;
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;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

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