for K being Field
for x being FinSequence of K
for a being Element of K st ex i being Element of NAT st
( 1 <= i & i <= len x & x . i = a & ( for j being Element of NAT st j <> i & 1 <= j & j <= len x holds
x . j = 0. K ) ) holds
Sum x = a