theorem :: GROUP_23:76

for I being non empty set
for G being Group
for F being normal Subgroup-Family of I,G
for A being Subset of G
for i being Element of I st A = union { the carrier of (F . j) where j is Element of I : i <> j } holds
ex N being strict normal Subgroup of G st N = gr A