let k, n be natural number ; :: thesis: ( k + n in Seg k implies n = 0 )
assume k + n in Seg k ; :: thesis: n = 0
then k + n <= k + 0 by FINSEQ_1:3;
hence n = 0 by XREAL_1:8; :: thesis: verum