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