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]

proof

let e be set ; :: thesis:
assume e in dom p ; :: thesis:
then reconsider l = e as Instruction-Location of S by A1, AMI_1:def 4;
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= dom the Object-Kind of S by A4, FUNCT_2:def 1;
for x being set st x in dom f holds
f . x in the Object-Kind of S . x

proof

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 Instruction-Location of S by A1, A4, A7, AMI_1:def 4;
the Object-Kind of S . y = ObjectKind y
.= the Instructions of S by AMI_1:def 14 ;
hence f . x in the Object-Kind of S . x by A8; :: thesis:

end;

then reconsider f = f as finite Element of sproduct the Object-Kind of S by A4, A6, CARD_3:def 9, FINSET_1:29;
reconsider f = f as FinPartState of S ;
take f ; :: thesis:
thus dom f = dom p by A4; :: thesis:
let m be natural number ; :: thesis:
assume il. S,m in dom p ; :: thesis:
then ex j being Element of NAT st
( il. S,m = il. S,j & f . (il. S,m) = IncAddr (pi p,(il. S,j)),k ) by A5;
hence f . (il. S,m) = IncAddr (pi p,(il. S,m)),k ; :: thesis: