theorem :: GROUP_1A:267

for G being addGroup
for a being Element of G
for H being finite Subgroup of G holds card H = card (H * a) by Th64;