let I be non empty set ; :: thesis: for G being Group
for F being normal Subgroup-Family of I,G
for A being Subset of G
for i being Element of I st A = union { the carrier of (F . j) where j is Element of I : i <> j } holds
ex N being strict normal Subgroup of G st N = gr A
let G be Group; :: thesis: for F being normal Subgroup-Family of I,G
for A being Subset of G
for i being Element of I st A = union { the carrier of (F . j) where j is Element of I : i <> j } holds
ex N being strict normal Subgroup of G st N = gr A
let F be normal Subgroup-Family of I,G; :: thesis: for A being Subset of G
for i being Element of I st A = union { the carrier of (F . j) where j is Element of I : i <> j } holds
ex N being strict normal Subgroup of G st N = gr A
let A be Subset of G; :: thesis: for i being Element of I st A = union { the carrier of (F . j) where j is Element of I : i <> j } holds
ex N being strict normal Subgroup of G st N = gr A
let i be Element of I; :: thesis: ( A = union { the carrier of (F . j) where j is Element of I : i <> j } implies ex N being strict normal Subgroup of G st N = gr A )
set X1 = { the carrier of (F . j) where j is Element of I : i <> j } ;
assume A1: A = union { the carrier of (F . j) where j is Element of I : i <> j } ; :: thesis: ex N being strict normal Subgroup of G st N = gr A
set J = I \ {i};

per cases ( I \ {i} is empty or not I \ {i} is empty ) ;

suppose I \ {i} is empty ; :: thesis: ex N being strict normal Subgroup of G st N = gr A

then ( I <> {} & I c= {i} ) by XBOOLE_1:37;
then A3: I = {i} by ZFMISC_1:33;
for x being object holds not x in { the carrier of (F . j) where j is Element of I : i <> j }

proof

given x being object such that A0: x in { the carrier of (F . j) where j is Element of I : i <> j } ; :: thesis: contradiction
ex j being Element of I st
( x = the carrier of (F . j) & i <> j ) by A0;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;

then { the carrier of (F . j) where j is Element of I : i <> j } = {} by XBOOLE_0:def 1;
then A4: A = {} the carrier of G by A1, ZFMISC_1:2, SUBSET_1:def 2;
take N = (1). G; :: thesis: N = gr A
thus N = gr A by A4, GROUP_4:30; :: thesis: verum

end;

suppose not I \ {i} is empty ; :: thesis: ex N being strict normal Subgroup of G st N = gr A

then reconsider J = I \ {i} as non empty set ;
reconsider FF = F | J as Subgroup-Family of J,G by ThSubFamRes;
for j being Element of J holds FF . j is normal Subgroup of G

proof

let j be Element of J; :: thesis: FF . j is normal Subgroup of G
j in I by XBOOLE_0:def 5;
then F . j is normal Subgroup of G by ThS1;
hence FF . j is normal Subgroup of G by FUNCT_1:49; :: thesis: verum

end;

then reconsider FF = FF as normal Subgroup-Family of J,G by ThS1;
set X2 = { the carrier of (FF . j) where j is Element of J : verum } ;
for x being object holds
( x in { the carrier of (F . j) where j is Element of I : i <> j } iff x in { the carrier of (FF . j) where j is Element of J : verum } )

proof

let x be object ; :: thesis: ( x in { the carrier of (F . j) where j is Element of I : i <> j } iff x in { the carrier of (FF . j) where j is Element of J : verum } )

hereby :: thesis: ( x in { the carrier of (FF . j) where j is Element of J : verum } implies x in { the carrier of (F . j) where j is Element of I : i <> j } )

assume x in { the carrier of (F . j) where j is Element of I : i <> j } ; :: thesis: x in { the carrier of (FF . j) where j is Element of J : verum }
then consider j being Element of I such that
Z1: ( x = the carrier of (F . j) & i <> j ) ;
( j in I & not j in {i} ) by Z1, TARSKI:def 1;
then reconsider jj = j as Element of J by XBOOLE_0:def 5;
F . j = FF . jj by FUNCT_1:49;
hence x in { the carrier of (FF . j) where j is Element of J : verum } by Z1; :: thesis: verum

end;

assume x in { the carrier of (FF . j) where j is Element of J : verum } ; :: thesis: x in { the carrier of (F . j) where j is Element of I : i <> j }
then consider j being Element of J such that
Z1: x = the carrier of (FF . j) ;
( j in I & not j in {i} ) by XBOOLE_0:def 5;
then Z2: ( j in I & j <> i ) by TARSKI:def 1;
then reconsider ii = j as Element of I ;
the carrier of (F . ii) = x by Z1, FUNCT_1:49;
hence x in { the carrier of (F . j) where j is Element of I : i <> j } by Z2; :: thesis: verum

end;

then A3: { the carrier of (F . j) where j is Element of I : i <> j } = { the carrier of (FF . j) where j is Element of J : verum } by TARSKI:2;
then reconsider B = union { the carrier of (FF . j) where j is Element of J : verum } as Subset of G by A1;
consider N being strict normal Subgroup of G such that
A2: N = gr B by ThJoinNorm;
take N ; :: thesis: N = gr A
thus N = gr A by A1, A2, A3; :: thesis: verum

end;

end;