theorem ThInjectiveIPO: :: GROUP_23:92

for G being Group
for I being non empty set
for F being normal Subgroup-Family of I,G st F is one-to-one 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 \ {i} holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G ) ) )