theorem :: GROUP_10:17

for G being Group
for A being non empty Subset of G
for g being Element of G holds card A = card (A * g) by Lm7;