defpred S₁[ set , set ] means ex m being Element of NAT st
( $1 = m & $2 = IncAddr ((p /. m),k) );
A2: for e being set st e in dom p holds
ex u being set st S₁[e,u]

proof

let e be set ; :: thesis: ( e in dom p implies ex u being set st S₁[e,u] )
assume e in dom p ; :: thesis: ex u being set st S₁[e,u]
then reconsider l = e as Element of NAT by A1;
consider m being natural number such that
A3: l = m ;
take IncAddr ((p /. m),k) ; :: thesis: S₁[e, IncAddr ((p /. m),k)]
thus S₁[e, IncAddr ((p /. m),k)] by A3; :: thesis: verum

end;

consider f being Function such that
A4: dom f = dom p and
A5: for e being set st e in dom p holds
S₁[e,f . e] from CLASSES1:sch 1(A2);
XX: rng f c= the Instructions of S

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in rng f or e in the Instructions of S )
assume e in rng f ; :: thesis: e in the Instructions of S
then consider u being set such that
W1: u in dom f and
W2: e = f . u by FUNCT_1:def 3;
S₁[u,f . u] by W1, A5, A4;
hence e in the Instructions of S by W2; :: thesis: verum

end;

reconsider f = f as NAT -defined the Instructions of S -valued finite Function by A1, A4, XX, FINSET_1:10, RELAT_1:def 18, RELAT_1:def 19;
take f ; :: thesis: ( dom f = dom p & ( for m being natural number st m in dom p holds
f . m = IncAddr ((p /. m),k) ) )
thus dom f = dom p by A4; :: thesis: for m being natural number st m in dom p holds
f . m = IncAddr ((p /. m),k)
let m be natural number ; :: thesis: ( m in dom p implies f . m = IncAddr ((p /. m),k) )
assume m in dom p ; :: thesis: f . m = IncAddr ((p /. m),k)
then ex j being Element of NAT st
( m = j & f . m = IncAddr ((p /. j),k) ) by A5;
hence f . m = IncAddr ((p /. m),k) ; :: thesis: verum