let O be set ; :: thesis: for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G ex N being strict normal StableSubgroup of G st the carrier of N = (carr N1) * (carr N2)
let G be GroupWithOperators of O; :: thesis: for N1, N2 being strict normal StableSubgroup of G ex N being strict normal StableSubgroup of G st the carrier of N = (carr N1) * (carr N2)
let N1, N2 be strict normal StableSubgroup of G; :: thesis: ex N being strict normal StableSubgroup of G st the carrier of N = (carr N1) * (carr N2)
set N19 = multMagma(# the carrier of N1,the multF of N1 #);
set N29 = multMagma(# the carrier of N2,the multF of N2 #);
reconsider N19 = multMagma(# the carrier of N1,the multF of N1 #), N29 = multMagma(# the carrier of N2,the multF of N2 #) as strict normal Subgroup of G by Lm7;
set A = (carr N19) * (carr N29);
set B = carr N19;
set C = carr N29;
(carr N19) * (carr N29) = (carr N29) * (carr N19) by GROUP_3:148;
then consider H9 being strict Subgroup of G such that
A1: the carrier of H9 = (carr N19) * (carr N29) by GROUP_2:93;

A2: now

let o be Element of O; :: thesis: for g being Element of G st g in (carr N19) * (carr N29) holds
(G ^ o) . g in (carr N19) * (carr N29)
let g be Element of G; :: thesis: ( g in (carr N19) * (carr N29) implies (G ^ o) . g in (carr N19) * (carr N29) )
assume g in (carr N19) * (carr N29) ; :: thesis: (G ^ o) . g in (carr N19) * (carr N29)
then consider a, b being Element of G such that
A3: g = a * b and
A4: a in carr N1 and
A5: b in carr N2 ;
a in N1 by A4, STRUCT_0:def 5;
then (G ^ o) . a in N1 by Lm10;
then A6: (G ^ o) . a in carr N1 by STRUCT_0:def 5;
b in N2 by A5, STRUCT_0:def 5;
then (G ^ o) . b in N2 by Lm10;
then (G ^ o) . b in carr N2 by STRUCT_0:def 5;
then ((G ^ o) . a) * ((G ^ o) . b) in (carr N1) * (carr N2) by A6;
hence (G ^ o) . g in (carr N19) * (carr N29) by A3, GROUP_6:def 7; :: thesis: verum

end;

A7: now

let g be Element of G; :: thesis: ( g in (carr N19) * (carr N29) implies g " in (carr N19) * (carr N29) )
assume g in (carr N19) * (carr N29) ; :: thesis: g " in (carr N19) * (carr N29)
then g in H9 by A1, STRUCT_0:def 5;
then g " in H9 by GROUP_2:60;
hence g " in (carr N19) * (carr N29) by A1, STRUCT_0:def 5; :: thesis: verum

end;

now

let g1, g2 be Element of G; :: thesis: ( g1 in (carr N19) * (carr N29) & g2 in (carr N19) * (carr N29) implies g1 * g2 in (carr N19) * (carr N29) )
assume ( g1 in (carr N19) * (carr N29) & g2 in (carr N19) * (carr N29) ) ; :: thesis: g1 * g2 in (carr N19) * (carr N29)
then ( g1 in H9 & g2 in H9 ) by A1, STRUCT_0:def 5;
then g1 * g2 in H9 by GROUP_2:59;
hence g1 * g2 in (carr N19) * (carr N29) by A1, STRUCT_0:def 5; :: thesis: verum

end;

then consider H being strict StableSubgroup of G such that
A8: the carrier of H = (carr N19) * (carr N29) by A1, A7, A2, Lm15;

now

let a be Element of G; :: thesis: a * H9 = H9 * a
thus a * H9 = (a * N19) * (carr N29) by A1, GROUP_2:35
.= (N19 * a) * (carr N29) by GROUP_3:140
.= (carr N19) * (a * N29) by GROUP_2:36
.= (carr N19) * (N29 * a) by GROUP_3:140
.= H9 * a by A1, GROUP_2:37 ; :: thesis: verum

end;

then H9 is normal Subgroup of G by GROUP_3:140;
then for H99 being strict Subgroup of G st H99 = multMagma(# the carrier of H,the multF of H #) holds
H99 is normal by A1, A8, GROUP_2:68;
then H is normal by Def10;
hence ex N being strict normal StableSubgroup of G st the carrier of N = (carr N1) * (carr N2) by A8; :: thesis: verum