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;

A8: the carrier of H = (carr N19) * (carr N29) by A1, A7, A2, Lm14;

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

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)

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;(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

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

g " in (carr N19) * (carr N29)

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;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

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)

then consider H being strict StableSubgroup of G such that 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;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

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

then
H9 is normal Subgroup of G
by GROUP_3:117;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;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

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