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