let G be Group; :: thesis: for I being non empty set
for F being Subgroup-Family of I,G holds
( G is_internal_product_of F iff ( ( for i being Element of I holds F . i is normal Subgroup of G ) & multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being Element of I
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G ) ) )
let I be non empty set ; :: thesis: for F being Subgroup-Family of I,G holds
( G is_internal_product_of F iff ( ( for i being Element of I holds F . i is normal Subgroup of G ) & multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being Element of I
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G ) ) )
let F be Subgroup-Family of I,G; :: thesis: ( G is_internal_product_of F iff ( ( for i being Element of I holds F . i is normal Subgroup of G ) & multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being Element of I
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G ) ) )
thus ( G is_internal_product_of F implies ( ( for i being Element of I holds F . i is normal Subgroup of G ) & multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being Element of I
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G ) ) ) :: thesis: ( ( for i being Element of I holds F . i is normal Subgroup of G ) & multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being Element of I
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G ) implies G is_internal_product_of F )

proof

assume A1: G is_internal_product_of F ; :: thesis: ( ( for i being Element of I holds F . i is normal Subgroup of G ) & multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being Element of I
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G ) )
thus for i being Element of I holds F . i is normal Subgroup of G by A1; :: thesis: ( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being Element of I
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G ) )
thus multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) by A1; :: thesis: for i being Element of I
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G
let i be Element of I; :: thesis: for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G
let J be Subset of I; :: thesis: ( J = I \ { j where j is Element of I : F . i = F . j } implies for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G )
assume A3: J = I \ { j where j is Element of I : F . i = F . j } ; :: thesis: for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G
let N be strict normal Subgroup of G; :: thesis: ( N = gr (Union (Carrier (F | J))) implies (F . i) /\ N = (1). G )
assume A4: N = gr (Union (Carrier (F | J))) ; :: thesis: (F . i) /\ N = (1). G
(F /. i) /\ N = (1). G by A1, A3, A4;
hence (F . i) /\ N = (1). G by Def20; :: thesis: verum

end;

assume A0: for i being Element of I holds F . i is normal Subgroup of G ; :: thesis: ( not multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) or ex i being Element of I ex J being Subset of I st
( J = I \ { j where j is Element of I : F . i = F . j } & ex N being strict normal Subgroup of G st
( N = gr (Union (Carrier (F | J))) & not (F . i) /\ N = (1). G ) ) or G is_internal_product_of F )
assume A1: multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) ; :: thesis: ( ex i being Element of I ex J being Subset of I st
( J = I \ { j where j is Element of I : F . i = F . j } & ex N being strict normal Subgroup of G st
( N = gr (Union (Carrier (F | J))) & not (F . i) /\ N = (1). G ) ) or G is_internal_product_of F )
assume A2: for i being Element of I
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G ; :: thesis: G is_internal_product_of F
reconsider I0 = I as set ;
reconsider F0 = F as Subgroup-Family of I0,G ;
for i0 being Element of I0
for J0 being Subset of I0 st J0 = I0 \ { j where j is Element of I : F . i0 = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F0 | J0))) holds
(F0 /. i0) /\ N = (1). G

proof

let i0 be Element of I0; :: thesis: for J0 being Subset of I0 st J0 = I0 \ { j where j is Element of I : F . i0 = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F0 | J0))) holds
(F0 /. i0) /\ N = (1). G
let J0 be Subset of I0; :: thesis: ( J0 = I0 \ { j where j is Element of I : F . i0 = F . j } implies for N being strict normal Subgroup of G st N = gr (Union (Carrier (F0 | J0))) holds
(F0 /. i0) /\ N = (1). G )
assume B2: J0 = I0 \ { j where j is Element of I : F . i0 = F . j } ; :: thesis: for N being strict normal Subgroup of G st N = gr (Union (Carrier (F0 | J0))) holds
(F0 /. i0) /\ N = (1). G
let N be strict normal Subgroup of G; :: thesis: ( N = gr (Union (Carrier (F0 | J0))) implies (F0 /. i0) /\ N = (1). G )
assume B3: N = gr (Union (Carrier (F0 | J0))) ; :: thesis: (F0 /. i0) /\ N = (1). G
reconsider i = i0 as Element of I ;
reconsider J = I \ { j where j is Element of I : F . i = F . j } as Subset of I ;
(F . i) /\ N = (1). G by A2, B2, B3;
hence (F0 /. i0) /\ N = (1). G by Def20; :: thesis: verum

end;

hence G is_internal_product_of F by A0, A1; :: thesis: verum