A1: k in NAT by ORDINAL1:def 13;
dom P = NAT by PARTFUN1:def 4;
then A2: P . k in rng P by A1, FUNCT_1:12;
rng P c= the Instructions of S by RELAT_1:def 19;
hence P . k is Instruction of S by A2; :: thesis: verum