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