for L being non empty Abelian add-associative addLoopStr
for a being Element of L
for p, q being FinSequence of the carrier of L st len p = len q & ex i being Element of NAT st
( i in dom p & q /. i = a + (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds
q /. i9 = p /. i9 ) ) holds
Sum q = a + (Sum p)