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