theorem Th7: :: RLAFFIN1:7

for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for g being Element of G
for A being Subset of G holds card A = card (g + A)