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

proof

let e be object ; :: thesis: ( e in dom p implies ex u being object st S₁[e,u] )
assume e in dom p ; :: thesis: ex u being object st S₁[e,u]
then reconsider l = e as Element of NAT by A1;
consider m being Nat 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 object st e in dom p holds
S₁[e,f . e] from CLASSES1:sch 1(A2);
A6: rng f c= the InstructionsF of S

proof

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

end;

reconsider f = f as NAT -defined the InstructionsF of S -valued finite Function by A1, A4, A6, FINSET_1:10, RELAT_1:def 18, RELAT_1:def 19;
take f ; :: thesis: ( dom f = dom p & ( for m being Nat st m in dom p holds
f . m = IncAddr ((p /. m),k) ) )
thus dom f = dom p by A4; :: thesis: for m being Nat st m in dom p holds
f . m = IncAddr ((p /. m),k)
let m be Nat; :: 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