let k, n be Nat; :: 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:1;
hence n = 0 by XREAL_1:6; :: thesis: verum