theorem :: GROUP_8:16

for G being Group
for A being non empty Subset of G
for x being Element of G holds card A = card (((x ") * A) * x)