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