for k, n, i being Nat st 1 <= k holds
( i in Seg n iff k * i in Seg (k * n) )