theorem :: GROUP_23:99

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
( G is_internal_product_of F iff G is_internal_product_of Fam )