theorem :: MOEBIUS1:2

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