:: deftheorem defines product GROUP_23:def 15 :
for I being non empty set
for F being Group-Family of I
for S being Subgroup-Family of F holds product S = product S;