let G be Group; for H being Subgroup of G
for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H )
let H be Subgroup of G; for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H )
let N1, N2 be strict normal Subgroup of G; ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H )
consider N being strict normal Subgroup of G such that
A1:
the carrier of N = N1 * N2
by Th8;
(N1 ~ H) * (N2 ~ H) c= N ~ H
proof
let x be
object ;
TARSKI:def 3 ( not x in (N1 ~ H) * (N2 ~ H) or x in N ~ H )
assume A2:
x in (N1 ~ H) * (N2 ~ H)
;
x in N ~ H
then reconsider x =
x as
Element of
G ;
consider a,
b being
Element of
G such that A3:
(
x = a * b &
a in N1 ~ H &
b in N2 ~ H )
by A2;
A4:
a * N1 meets carr H
by A3, Th51;
A5:
b * N2 meets carr H
by A3, Th51;
consider x1 being
object such that A6:
(
x1 in a * N1 &
x1 in carr H )
by A4, XBOOLE_0:3;
consider x2 being
object such that A7:
(
x2 in b * N2 &
x2 in carr H )
by A5, XBOOLE_0:3;
reconsider x1 =
x1 as
Element of
G by A6;
reconsider x2 =
x2 as
Element of
G by A7;
A8:
x1 * x2 in (carr H) * (carr H)
by A6, A7;
A9:
x1 * x2 in (a * N1) * (b * N2)
by A6, A7;
(carr H) * (carr H) = carr H
by GROUP_2:76;
then A10:
(a * N1) * (b * N2) meets carr H
by A8, A9, XBOOLE_0:3;
(a * N1) * (b * N2) = (a * b) * N
by A1, Th10;
hence
x in N ~ H
by A3, A10;
verum
end;
hence
ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H )
by A1; verum