theorem Th147: :: GROUP_1A:193

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