theorem :: VALUED_1:26

for p being Function st dom p c= NAT holds
for k being Nat holds rng (Shift (p,k)) = rng p