theorem ThIPOa: :: GROUP_23:90

for G being Group
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 ) ) )