let k, n be Nat; :: thesis: ( k <> 0 implies k in Seg (k + n) )
assume k <> 0 ; :: thesis: k in Seg (k + n)
then A1: 0 + 1 <= k by NAT_1:13;
k <= k + n by NAT_1:12;
hence k in Seg (k + n) by A1, FINSEQ_1:1; :: thesis: verum