theorem Th24: :: VALUED_1:24

for p being Function
for k, il being Nat st il in dom p holds
il + k in dom (Shift (p,k))