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