let G be Group; :: thesis: 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; :: thesis: 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; :: thesis: 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

( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H ) by A1; :: thesis: verum

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

hence
ex N being strict normal Subgroup of G st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (N1 ~ H) * (N2 ~ H) or x in N ~ H )

assume A2: x in (N1 ~ H) * (N2 ~ H) ; :: thesis: 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; :: thesis: verum

end;assume A2: x in (N1 ~ H) * (N2 ~ H) ; :: thesis: 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; :: thesis: verum

( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H ) by A1; :: thesis: verum