theorem :: VALUED_1:20

for P, Q being Function
for k being Nat st P c= Q holds
Shift (P,k) c= Shift (Q,k)