let G be Group; :: thesis: for I being non empty set
for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of (Subgroups G) st Fam = rng F holds
( G is_internal_product_of F iff G is_internal_product_of Fam )
let I be non empty set ; :: thesis: for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of (Subgroups G) st Fam = rng F holds
( G is_internal_product_of F iff G is_internal_product_of Fam )
let F be componentwise_strict Subgroup-Family of I,G; :: thesis: for Fam being Subset of (Subgroups G) st Fam = rng F holds
( G is_internal_product_of F iff G is_internal_product_of Fam )
let Fam be Subset of (Subgroups G); :: thesis: ( Fam = rng F implies ( G is_internal_product_of F iff G is_internal_product_of Fam ) )
assume A1: Fam = rng F ; :: thesis: ( G is_internal_product_of F iff G is_internal_product_of Fam )
thus ( G is_internal_product_of F implies G is_internal_product_of Fam ) :: thesis: ( G is_internal_product_of Fam implies G is_internal_product_of F )

proof

assume B1: G is_internal_product_of F ; :: thesis: G is_internal_product_of Fam
B2: for H being strict Subgroup of G st H in Fam holds
H is normal Subgroup of G

proof

let H be strict Subgroup of G; :: thesis: ( H in Fam implies H is normal Subgroup of G )
assume H in Fam ; :: thesis: H is normal Subgroup of G
then consider i being Element of I such that
Z1: H = F . i by A1, MssRng;
thus H is normal Subgroup of G by B1, Z1; :: thesis: verum

end;

B3: ex A being Subset of G st
( A = union { UH where UH is Subset of G : ex H being strict Subgroup of G st
( H in Fam & UH = the carrier of H ) } & multMagma(# the carrier of G, the multF of G #) = gr A )

proof

consider A being Subset of G such that
Z1: A = Union (Carrier F) ;
take A ; :: thesis: ( A = union { UH where UH is Subset of G : ex H being strict Subgroup of G st
( H in Fam & UH = the carrier of H ) } & multMagma(# the carrier of G, the multF of G #) = gr A )
thus union { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } = A by A1, Z1, ThCarrG; :: thesis: multMagma(# the carrier of G, the multF of G #) = gr A
thus multMagma(# the carrier of G, the multF of G #) = gr A by Z1, B1; :: thesis: verum

end;

for H being strict Subgroup of G st H in Fam holds
for A being Subset of G st A = union { UK where UK is Subset of G : ex K being strict Subgroup of G st
( K in Fam & UK = the carrier of K & K <> H ) } holds
H /\ (gr A) = (1). G

proof

let H be strict Subgroup of G; :: thesis: ( H in Fam implies for A being Subset of G st A = union { UK where UK is Subset of G : ex K being strict Subgroup of G st
( K in Fam & UK = the carrier of K & K <> H ) } holds
H /\ (gr A) = (1). G )
assume Z1: H in Fam ; :: thesis: for A being Subset of G st A = union { UK where UK is Subset of G : ex K being strict Subgroup of G st
( K in Fam & UK = the carrier of K & K <> H ) } holds
H /\ (gr A) = (1). G
let A be Subset of G; :: thesis: ( A = union { UK where UK is Subset of G : ex K being strict Subgroup of G st
( K in Fam & UK = the carrier of K & K <> H ) } implies H /\ (gr A) = (1). G )
assume Z2: A = union { UK where UK is Subset of G : ex K being strict Subgroup of G st
( K in Fam & UK = the carrier of K & K <> H ) } ; :: thesis: H /\ (gr A) = (1). G
consider i being Element of I such that
Z3: H = F . i by A1, Z1, MssRng;
reconsider J = I \ { j where j is Element of I : F . i = F . j } as Subset of I ;
for i being Element of I holds F . i is normal Subgroup of G by B1;
then F is normal Subgroup-Family of I,G by ThS1;
then consider N being strict normal Subgroup of G such that
Z5: N = gr (Union (Carrier (F | J))) by ThJoinNormUnionRes;
( H = F /. i & (F /. i) /\ N = (1). G ) by B1, Z3, Z5, Def20;
hence H /\ (gr A) = (1). G by A1, Z2, Z3, Z5, ThUnionFam; :: thesis: verum

end;

hence G is_internal_product_of Fam by B2, B3; :: thesis: verum

end;

assume B1: G is_internal_product_of Fam ; :: thesis: G is_internal_product_of F
B2: for i being Element of I holds F . i is normal Subgroup of G

proof

let i be Element of I; :: thesis: F . i is normal Subgroup of G
( F . i is Subgroup of G & F . i is strict Subgroup of G ) by ThS2;
hence F . i is normal Subgroup of G by A1, B1, MssRng; :: thesis: verum

end;

for i being Element of I
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | (I \ { j where j is Element of I : F . i = F . j } )))) holds
(F /. i) /\ N = (1). G

proof

let i be Element of I; :: thesis: for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | (I \ { j where j is Element of I : F . i = F . j } )))) holds
(F /. i) /\ N = (1). G
let N be strict normal Subgroup of G; :: thesis: ( N = gr (Union (Carrier (F | (I \ { j where j is Element of I : F . i = F . j } )))) implies (F /. i) /\ N = (1). G )
assume Z2: N = gr (Union (Carrier (F | (I \ { j where j is Element of I : F . i = F . j } )))) ; :: thesis: (F /. i) /\ N = (1). G
reconsider H = F . i as strict Subgroup of G by Def19;
reconsider H = H as strict normal Subgroup of G by A1, B1, MssRng;
reconsider J = I \ { j where j is Element of I : F . i = F . j } as Subset of I ;
Z4: union { A0 where A0 is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A0 = the carrier of K & K <> H ) } = Union (Carrier (F | J)) by A1, ThUnionFam;
then reconsider A = union { A0 where A0 is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A0 = the carrier of K & K <> H ) } as Subset of G ;
H /\ N = (1). G by A1, B1, Z2, Z4, MssRng;
hence (F /. i) /\ N = (1). G by Def20; :: thesis: verum

end;

hence G is_internal_product_of F by A1, B1, B2, ThCarrG; :: thesis: verum