for m being Element of NAT
for K being Field
for x, y being FinSequence of K
for i being Element of NAT st len x = m & y = mlt (x,(Base_FinSeq (K,m,i))) & 1 <= i & i <= m holds
( y . i = x . i & ( for j being Element of NAT st j <> i & 1 <= j & j <= m holds
y . j = 0. K ) )