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: dom p c= NAT by RELAT_1:def 18;
then dom p c= the carrier of SCM+FSA by XBOOLE_1:1;
then A6: dom f c= dom the Object-Kind of SCM+FSA by A3, FUNCT_2:def 1;
for x being set st x in dom f holds
f . x in the Object-Kind of SCM+FSA . x

proof

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

end;

then reconsider f = f as Element of sproduct the Object-Kind of SCM+FSA by A6, CARD_3:def 9;
reconsider f = f as FinPartState of SCM+FSA by A3, FINSET_1:29;
B: f is the Instructions of SCM+FSA -valued

proof

let x be set ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not x in proj2 f or x in the Instructions of SCM+FSA )
assume x in rng f ; :: thesis: x in the Instructions of SCM+FSA
then consider y being set such that
W1: y in dom f and
W2: f . y = x by FUNCT_1:def 5;
reconsider y = y as Element of NAT by W1, A3, A5;
y in dom p by A3, W1;
then S₁[y,x] by A4, W2;
then consider m being Element of NAT such that
W3: ( y = m & x = IncAddr (p /. m),k ) ;
x = IncAddr (p /. m),k by W3;
hence x in the Instructions of SCM+FSA ; :: thesis: verum

end;

f is NAT -defined

proof

let x be set ; :: according to TARSKI:def 3,RELAT_1:def 18 :: thesis: ( not x in proj1 f or x in NAT )
assume x in dom f ; :: thesis: x in NAT
hence x in NAT by A3, A5; :: thesis: verum

end;

then reconsider IT = f as preProgram of SCM+FSA by B;
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