for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for A being finite Subset of V
for E being Enumeration of A
for v being Element of V holds E + ((card A) |-> v) is Enumeration of v + A