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 st A = union { the carrier of (F . i) where i is Element of I : verum } 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 st A = union { the carrier of (F . i) where i is Element of I : verum } 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 st A = union { the carrier of (F . i) where i is Element of I : verum } holds
ex N being strict normal Subgroup of G st N = gr A
let A be Subset of G; :: thesis: ( A = union { the carrier of (F . i) where i is Element of I : verum } implies ex N being strict normal Subgroup of G st N = gr A )
set X = { the carrier of (F . i) where i is Element of I : verum } ;
assume A1: A = union { the carrier of (F . i) where i is Element of I : verum } ; :: thesis: ex N being strict normal Subgroup of G st N = gr A
reconsider N = gr A as strict Subgroup of G ;
A2: for i being Element of I holds the carrier of (F . i) c= the carrier of N

proof

let i be Element of I; :: thesis: the carrier of (F . i) c= the carrier of N
the carrier of (F . i) in { the carrier of (F . i) where i is Element of I : verum } ;
then B1: the carrier of (F . i) c= A by A1, ZFMISC_1:74;
A c= the carrier of N by GROUP_4:def 4;
hence the carrier of (F . i) c= the carrier of N by B1, XBOOLE_1:1; :: thesis: verum

end;

for a being Element of G holds N |^ a is Subgroup of N

proof

let a be Element of G; :: thesis: N |^ a is Subgroup of N
for g being Element of G st g in N |^ a holds
g in N

proof

let g be Element of G; :: thesis: ( g in N |^ a implies g in N )
assume g in N |^ a ; :: thesis: g in N
then consider x being Element of G such that
A4: ( g = x |^ a & x in N ) by GROUP_3:58;
consider FS being FinSequence of the carrier of G, ks being FinSequence of INT such that
A5: ( len FS = len ks & rng FS c= A & Product (FS |^ ks) = x ) by A4, GROUP_4:28;
A6: Product ((FS |^ ks) |^ a) = Product ((FS |^ a) |^ ks) by GROUP_5:15;
for y being object st y in rng ((FS |^ a) |^ ks) holds
y in carr N

proof

let y be object ; :: thesis: ( y in rng ((FS |^ a) |^ ks) implies y in carr N )
assume y in rng ((FS |^ a) |^ ks) ; :: thesis: y in carr N
then consider xi being object such that
A7: ( xi in dom ((FS |^ a) |^ ks) & y = ((FS |^ a) |^ ks) . xi ) by FUNCT_1:def 3;
A8: len ((FS |^ a) |^ ks) = len ((FS |^ ks) |^ a) by GROUP_5:15
.= len (FS |^ ks) by GROUP_5:def 1 ;
A9: dom ((FS |^ a) |^ ks) = Seg (len (FS |^ ks)) by A8, FINSEQ_1:def 3
.= dom (FS |^ ks) by FINSEQ_1:def 3 ;
reconsider xi = xi as Nat by A7;
A10: dom (FS |^ ks) = Seg (len (FS |^ ks)) by FINSEQ_1:def 3
.= Seg (len FS) by GROUP_4:def 3
.= dom FS by FINSEQ_1:def 3 ;
FS . xi in rng FS by A7, A9, A10, FUNCT_1:3;
then consider Fi being set such that
A11: ( FS . xi in Fi & Fi in { the carrier of (F . i) where i is Element of I : verum } ) by A1, A5, TARSKI:def 4;
consider i0 being Element of I such that
A12: Fi = the carrier of (F . i0) by A11;
FS /. xi in F . i0 by A10, A7, A9, A11, A12, PARTFUN1:def 6;
then (FS /. xi) |^ (@ (ks /. xi)) in F . i0 by GROUP_4:4;
then (FS |^ ks) . xi in F . i0 by A7, A9, A10, GROUP_4:def 3;
then (FS |^ ks) /. xi in F . i0 by A7, A9, PARTFUN1:def 6;
then A14: ((FS |^ ks) /. xi) |^ a in F . i0 by ThNorm;
y = ((FS |^ ks) |^ a) . xi by A7, GROUP_5:15
.= ((FS |^ ks) /. xi) |^ a by A7, A9, GROUP_5:def 1 ;
hence y in carr N by A2, A14, TARSKI:def 3; :: thesis: verum

end;

then Product ((FS |^ a) |^ ks) in N by GROUP_4:18, TARSKI:def 3;
hence g in N by A4, A5, A6, GROUP_5:14; :: thesis: verum

end;

hence N |^ a is Subgroup of N by GROUP_2:58; :: thesis: verum

end;

then reconsider N = N as strict normal Subgroup of G by GROUP_3:122;
take N ; :: thesis: N = gr A
thus N = gr A ; :: thesis: verum