let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (ProgramPart p) ; :: thesis:
then consider y being set such that
W1: y in dom (ProgramPart p) and
W2: x = (ProgramPart p) . y by FUNCT_1:def 5;
reconsider y = y as Instruction-Location of S by W1, A, AMI_1:def 4;
consider s being State of S such that
W3: p c= s by CARD_3:97;
dom (ProgramPart p) c= dom p by RELAT_1:89;
then p . y = s . y by W1, W3, GRFUNC_1:8;
then p . y in the Instructions of S ;
hence x in the Instructions of S by W2, W1, FUNCT_1:70; :: thesis:

end;