theorem ThUnionFam: :: GROUP_23:98

for G being Group
for I being non empty set
for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of (Subgroups G) st Fam = rng F holds
for H being strict Subgroup of G
for i being Element of I st H = F . i holds
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J))