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 Lm6;
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:125;
then consider H9 being strict Subgroup of G such that
A1: the carrier of H9 = (carr N19) * (carr N29) by GROUP_2:78;

A2: now :: thesis: for o being Element of O
for g being Element of G st g in (carr N19) * (carr N29) holds
(G ^ o) . g in (carr N19) * (carr N29)

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 Lm9;
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 Lm9;
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 6; :: thesis: verum

end;

A7: now :: thesis: for g being Element of G st g in (carr N19) * (carr N29) holds
g " in (carr N19) * (carr N29)

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:51;
hence g " in (carr N19) * (carr N29) by A1, STRUCT_0:def 5; :: thesis: verum

end;

now :: thesis: for g1, g2 being Element of G st g1 in (carr N19) * (carr N29) & g2 in (carr N19) * (carr N29) holds
g1 * g2 in (carr N19) * (carr N29)

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:50;
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, Lm14;

now :: thesis: for a being Element of G holds a * H9 = H9 * a

let a be Element of G; :: thesis: a * H9 = H9 * a
thus a * H9 = (a * N19) * (carr N29) by A1, GROUP_2:29
.= (N19 * a) * (carr N29) by GROUP_3:117
.= (carr N19) * (a * N29) by GROUP_2:30
.= (carr N19) * (N29 * a) by GROUP_3:117
.= H9 * a by A1, GROUP_2:31 ; :: thesis: verum

end;

then H9 is normal Subgroup of G by GROUP_3:117;
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:59;
then H is normal ;
hence ex N being strict normal StableSubgroup of G st the carrier of N = (carr N1) * (carr N2) by A8; :: thesis: verum