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