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

let e be set ; :: thesis:
assume e in dom p ; :: thesis:
then reconsider l = e as Element of NAT by A1;
consider m being natural number such that
A3: l = il. S,m by AMISTD_1:26;
take IncAddr (pi p,(il. S,m)),k ; :: thesis:
reconsider m = m as Element of NAT by ORDINAL1:def 13;
e = il. S,m by A3;
hence S₁[e, IncAddr (pi p,(il. S,m)),k] ; :: thesis:

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);
NAT c= the carrier of S by AMI_1:def 3;
then dom p c= the carrier of S by A1, XBOOLE_1:1;
then A6: dom f c= the carrier of S by A4;
for x being set st x in dom f holds
f . x in the Object-Kind of S . x

let x be set ; :: thesis:
assume A7: x in dom f ; :: thesis:
then A8: ex m being Element of NAT st
( x = il. S,m & f . x = IncAddr (pi p,(il. S,m)),k ) by A4, A5;
reconsider y = x as Element of NAT by A1, A4, A7;
the Object-Kind of S . y = the Instructions of S by AMI_1:def 14;
hence f . x in the Object-Kind of S . x by A8; :: thesis:

end;