theorem :: GROUP_3:66

for G being Group
for a being Element of G
for H being finite Subgroup of G holds card H = card (H |^ a) by Th64;