theorem :: GROUP_2:149

for G being finite Group
for I, H being Subgroup of G
for J being Subgroup of H st I = J holds
index I = (index J) * (index H)