A1: dom (ProgramPart p) c= NAT by RELAT_1:87;
rng (ProgramPart p) c= the Instructions of S

proof

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

end;

hence ProgramPart p is NAT -defined the Instructions of S -valued finite Function by A1, RELSET_1:11; :: thesis: verum