defpred S₁[ set , set ] means ex m being Element of NAT st
( $1 = m & $2 = IncAddr (p /. m),k );
A1: 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] )
A2: dom p c= NAT by RELAT_1:def 18;
assume e in dom p ; :: thesis: ex u being set st S₁[e,u]
then reconsider e = e as Element of NAT by A2;
reconsider m = e as Element of NAT ;
take IncAddr (p /. m),k ; :: thesis: S₁[e, IncAddr (p /. m),k]
thus S₁[e, IncAddr (p /. m),k] ; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in the Instructions of SCM )
assume x in rng f ; :: thesis: x in the Instructions of SCM
then consider y being set such that
A6: y in dom f and
A7: f . y = x by FUNCT_1:def 5;
ex m being Element of NAT st
( y = m & f . y = IncAddr (p /. m),k ) by A3, A4, A6;
hence x in the Instructions of SCM by A7; :: thesis: verum

end;

dom p c= NAT by RELAT_1:def 18;
then f is NAT -defined the Instructions of SCM -valued finite Function by A3, A5, FINSET_1:29, RELSET_1:11;
then reconsider IT = f as NAT -defined FinPartState of by AMI_1:148;
take IT ; :: thesis: ( dom IT = dom p & ( for m being Element of NAT st m in dom p holds
IT . m = IncAddr (p /. m),k ) )
thus dom IT = dom p by A3; :: thesis: for m being Element of NAT st m in dom p holds
IT . m = IncAddr (p /. m),k
let m be Element of NAT ; :: thesis: ( m in dom p implies IT . m = IncAddr (p /. m),k )
assume m in dom p ; :: thesis: IT . m = IncAddr (p /. m),k
then ex j being Element of NAT st
( m = j & f . m = IncAddr (p /. j),k ) by A4;
hence IT . m = IncAddr (p /. m),k ; :: thesis: verum