let G be Group; :: thesis: for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = (carr N1) * (carr N2)
let N1, N2 be strict normal Subgroup of G; :: thesis: ex N being strict normal Subgroup of G st the carrier of N = (carr N1) * (carr N2)
set A = (carr N1) * (carr N2);
set B = carr N1;
set C = carr N2;
(carr N1) * (carr N2) = (carr N2) * (carr N1) by Th125;
then consider H being strict Subgroup of G such that
A1: the carrier of H = (carr N1) * (carr N2) by GROUP_2:78;

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

let a be Element of G; :: thesis: a * H = H * a
thus a * H = (a * N1) * (carr N2) by A1, GROUP_2:29
.= (N1 * a) * (carr N2) by Th117
.= (carr N1) * (a * N2) by GROUP_2:30
.= (carr N1) * (N2 * a) by Th117
.= H * a by A1, GROUP_2:31 ; :: thesis: verum

end;

then H is normal Subgroup of G by Th117;
hence ex N being strict normal Subgroup of G st the carrier of N = (carr N1) * (carr N2) by A1; :: thesis: verum