dom p c= NAT by RELAT_1:def 18;
then reconsider loc = loc as Element of NAT by A1;
consider s being State of S such that
A2: p c= s by PBOOLE:156;
s . loc = p . loc by A1, A2, GRFUNC_1:8;
hence p . loc is Instruction of S ; :: thesis: verum