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 4
.= (x * a) * (b * (x " )) by GROUP_1:def 4
.= ((x * a) * (1_ G)) * (b * (x " )) by GROUP_1:def 5
.= ((x * a) * ((x " ) * x)) * (b * (x " )) by GROUP_1:def 6
.= (((x * a) * (x " )) * x) * (b * (x " )) by GROUP_1:def 4
.= ((x * a) * (x " )) * (x * (b * (x " ))) by GROUP_1:def 4
.= ((x * a) * (x " )) * ((x * b) * (x " )) by GROUP_1:def 4 ;
( (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