for K being Field
for i, n being Nat st 1 <= i & i <= n holds
(Base_FinSeq (K,n,i)) . i = 1. K