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 Element of NAT by A1, A2;
consider s being State of S such that
A4: p c= s by PBOOLE:156;
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 for b₁ being Function st b₁ = ProgramPart p holds
( b₁ is finite & b₁ is NAT -defined & b₁ is the Instructions of S -valued ) by A1, RELSET_1:11; :: thesis: verum