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