theorem :: GROUP_23:68

for I being non empty set
for F being Group-Family of I
for S being componentwise_strict normal Subgroup-Family of F holds (product F) ./. (product S), product (F ./. S) are_isomorphic