for L being non empty Abelian add-associative right_zeroed addLoopStr
for f being FinSequence of L
for i, j being Element of NAT holds Sum (Swap (f,i,j)) = Sum f