theorem :: VALUED_1:29

for F being Function
for k being Nat st k > 0 holds
not 0 in dom (Shift (F,k))