let G be Group; :: thesis: for A being non empty Subset 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 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )

let A be non empty Subset 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 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )

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 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )

consider N being strict normal Subgroup of G such that

A1: the carrier of N = N1 * N2 by Th8;

N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1)

( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) ) 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 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )

let A be non empty Subset 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 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )

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 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )

consider N being strict normal Subgroup of G such that

A1: the carrier of N = N1 * N2 by Th8;

N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1)

proof

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

assume A2: x in N ~ A ; :: thesis: x in ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1)

then reconsider x = x as Element of G ;

x * N meets A by A2, Th14;

then consider x1 being object such that

A3: ( x1 in x * N & x1 in A ) by XBOOLE_0:3;

reconsider x1 = x1 as Element of G by A3;

consider y being Element of G such that

A4: ( x1 = x * y & y in N ) by A3, GROUP_2:103;

A5: y in N1 * N2 by A1, A4, STRUCT_0:def 5;

then consider a, b being Element of G such that

A6: ( y = a * b & a in N1 & b in N2 ) by Th6;

A7: x1 = (x * a) * b by A4, A6, GROUP_1:def 3;

a in carr N1 by A6, STRUCT_0:def 5;

then A8: (x * a) * b in (x * N1) * b by GROUP_8:15;

(x * N1) * b = x * (N1 * b) by GROUP_2:106

.= x * (b * N1) by GROUP_3:117

.= (x * b) * N1 by GROUP_2:105 ;

then (x * b) * N1 meets A by A3, A7, A8, XBOOLE_0:3;

then A9: x * b in N1 ~ A ;

A10: (x * b) * (b ") = x * (b * (b ")) by GROUP_1:def 3

.= x * (1_ G) by GROUP_1:def 5

.= x by GROUP_1:def 4 ;

b " in N2 by A6, GROUP_2:51;

then A11: x in (N1 ~ A) * N2 by A9, A10, GROUP_2:94;

y in N2 * N1 by A5, GROUP_3:125;

then consider a, b being Element of G such that

A12: ( y = a * b & a in N2 & b in N1 ) by Th6;

A13: x1 = (x * a) * b by A4, A12, GROUP_1:def 3;

a in carr N2 by A12, STRUCT_0:def 5;

then A14: (x * a) * b in (x * N2) * b by GROUP_8:15;

(x * N2) * b = x * (N2 * b) by GROUP_2:106

.= x * (b * N2) by GROUP_3:117

.= (x * b) * N2 by GROUP_2:105 ;

then (x * b) * N2 meets A by A3, A13, A14, XBOOLE_0:3;

then A15: x * b in N2 ~ A ;

A16: (x * b) * (b ") = x * (b * (b ")) by GROUP_1:def 3

.= x * (1_ G) by GROUP_1:def 5

.= x by GROUP_1:def 4 ;

b " in N1 by A12, GROUP_2:51;

then x in (N2 ~ A) * N1 by A15, A16, GROUP_2:94;

hence x in ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) by A11, XBOOLE_0:def 4; :: thesis: verum

end;assume A2: x in N ~ A ; :: thesis: x in ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1)

then reconsider x = x as Element of G ;

x * N meets A by A2, Th14;

then consider x1 being object such that

A3: ( x1 in x * N & x1 in A ) by XBOOLE_0:3;

reconsider x1 = x1 as Element of G by A3;

consider y being Element of G such that

A4: ( x1 = x * y & y in N ) by A3, GROUP_2:103;

A5: y in N1 * N2 by A1, A4, STRUCT_0:def 5;

then consider a, b being Element of G such that

A6: ( y = a * b & a in N1 & b in N2 ) by Th6;

A7: x1 = (x * a) * b by A4, A6, GROUP_1:def 3;

a in carr N1 by A6, STRUCT_0:def 5;

then A8: (x * a) * b in (x * N1) * b by GROUP_8:15;

(x * N1) * b = x * (N1 * b) by GROUP_2:106

.= x * (b * N1) by GROUP_3:117

.= (x * b) * N1 by GROUP_2:105 ;

then (x * b) * N1 meets A by A3, A7, A8, XBOOLE_0:3;

then A9: x * b in N1 ~ A ;

A10: (x * b) * (b ") = x * (b * (b ")) by GROUP_1:def 3

.= x * (1_ G) by GROUP_1:def 5

.= x by GROUP_1:def 4 ;

b " in N2 by A6, GROUP_2:51;

then A11: x in (N1 ~ A) * N2 by A9, A10, GROUP_2:94;

y in N2 * N1 by A5, GROUP_3:125;

then consider a, b being Element of G such that

A12: ( y = a * b & a in N2 & b in N1 ) by Th6;

A13: x1 = (x * a) * b by A4, A12, GROUP_1:def 3;

a in carr N2 by A12, STRUCT_0:def 5;

then A14: (x * a) * b in (x * N2) * b by GROUP_8:15;

(x * N2) * b = x * (N2 * b) by GROUP_2:106

.= x * (b * N2) by GROUP_3:117

.= (x * b) * N2 by GROUP_2:105 ;

then (x * b) * N2 meets A by A3, A13, A14, XBOOLE_0:3;

then A15: x * b in N2 ~ A ;

A16: (x * b) * (b ") = x * (b * (b ")) by GROUP_1:def 3

.= x * (1_ G) by GROUP_1:def 5

.= x by GROUP_1:def 4 ;

b " in N1 by A12, GROUP_2:51;

then x in (N2 ~ A) * N1 by A15, A16, GROUP_2:94;

hence x in ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) by A11, XBOOLE_0:def 4; :: thesis: verum

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