theorem Th25: :: VALUED_1:25

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