theorem ThJoinNorm: :: GROUP_23:74

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 st A = union { the carrier of (F . i) where i is Element of I : verum } holds
ex N being strict normal Subgroup of G st N = gr A