for m, i being Element of NAT
for K being Field
for x being FinSequence of K st len x = m & 1 <= i & i <= m holds
( |(x,(Base_FinSeq (K,m,i)))| = x . i & |(x,(Base_FinSeq (K,m,i)))| = x /. i )