theorem Th5: :: NBVECTSP:5

for m being non zero Element of NAT
for x being FinSequence of Z_2
for v being Element of Z_2
for j being Nat st len x = m & j in Seg m & ( for i being Nat st i in Seg m holds
( ( i = j implies x . i = v ) & ( i <> j implies x . i = 0. Z_2 ) ) ) holds
Sum x = v