A1: dom (Shift p,k) c= NAT by RELAT_1:def 18;
dom p c= NAT by RELAT_1:def 18;
then rng (Shift p,k) = rng p by VALUED_1:27;
then rng (Shift p,k) c= the Instructions of S by RELAT_1:def 19;
hence Shift p,k is the Instructions of S -valued by A1, RELSET_1:11; :: thesis: verum