theorem :: GROUP_1A:195

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