let G be addGroup; :: 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 Lm5;
then consider H being strict Subgroup of G such that
A1: the carrier of H = (carr N1) + (carr N2) by Th78;

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, ThB29
.= (N1 + a) + (carr N2) by Th117
.= (carr N1) + (a + N2) by ThA30
.= (carr N1) + (N2 + a) by Th117
.= H + a by A1, ThB31 ; :: 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