theorem Th147: :: GROUP_2:147

for G being finite Group
for H being Subgroup of G holds card G = (card H) * (index H)