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 N1' = multMagma(# the carrier of N1,the multF of N1 #);
set N2' = multMagma(# the carrier of N2,the multF of N2 #);
reconsider N1' = multMagma(# the carrier of N1,the multF of N1 #), N2' = multMagma(# the carrier of N2,the multF of N2 #) as strict normal Subgroup of G by Lm7;
set A = (carr N1') * (carr N2');
set B = carr N1';
set C = carr N2';
(carr N1') * (carr N2') = (carr N2') * (carr N1') by GROUP_3:148;
then consider H' being strict Subgroup of G such that
A1: the carrier of H' = (carr N1') * (carr N2') by GROUP_2:93;

A2: now

let o be Element of O; :: thesis: for g being Element of st g in (carr N1') * (carr N2') holds
(G ^ o) . g in (carr N1') * (carr N2')
let g be Element of ; :: thesis: ( g in (carr N1') * (carr N2') implies (G ^ o) . g in (carr N1') * (carr N2') )
assume g in (carr N1') * (carr N2') ; :: thesis: (G ^ o) . g in (carr N1') * (carr N2')
then consider a, b being Element of 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 N1') * (carr N2') by A3, GROUP_6:def 7; :: thesis: verum

end;

A7: now

let g be Element of ; :: thesis: ( g in (carr N1') * (carr N2') implies g " in (carr N1') * (carr N2') )
assume g in (carr N1') * (carr N2') ; :: thesis: g " in (carr N1') * (carr N2')
then g in H' by A1, STRUCT_0:def 5;
then g " in H' by GROUP_2:60;
hence g " in (carr N1') * (carr N2') by A1, STRUCT_0:def 5; :: thesis: verum

end;

now

let g1, g2 be Element of ; :: thesis: ( g1 in (carr N1') * (carr N2') & g2 in (carr N1') * (carr N2') implies g1 * g2 in (carr N1') * (carr N2') )
assume ( g1 in (carr N1') * (carr N2') & g2 in (carr N1') * (carr N2') ) ; :: thesis: g1 * g2 in (carr N1') * (carr N2')
then ( g1 in H' & g2 in H' ) by A1, STRUCT_0:def 5;
then g1 * g2 in H' by GROUP_2:59;
hence g1 * g2 in (carr N1') * (carr N2') 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 N1') * (carr N2') by A1, A7, A2, Lm15;

now

let a be Element of ; :: thesis: a * H' = H' * a
thus a * H' = (a * N1') * (carr N2') by A1, GROUP_2:35
.= (N1' * a) * (carr N2') by GROUP_3:140
.= (carr N1') * (a * N2') by GROUP_2:36
.= (carr N1') * (N2' * a) by GROUP_3:140
.= H' * a by A1, GROUP_2:37 ; :: thesis: verum

end;

then H' is normal Subgroup of G by GROUP_3:140;
then for H'' being strict Subgroup of G st H'' = multMagma(# the carrier of H,the multF of H #) holds
H'' 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