let G be Group; :: thesis: for I being non empty set
for F being normal Subgroup-Family of I,G holds
( G is_internal_product_of F iff ( 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 normal Subgroup-Family of I,G holds
( G is_internal_product_of F iff ( 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 normal Subgroup-Family of I,G; :: thesis: ( G is_internal_product_of F iff ( 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 ( 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 ) ) ) by ThIPOa; :: 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 ) implies 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
for i being Element of I holds F . i is normal Subgroup of G ;
hence G is_internal_product_of F by A1, A2, ThIPOa; :: thesis: verum