defpred S₁[ set , set ] means ex m being Element of NAT st
( $1 = m & $2 = IncAddr (pi 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 (pi p,m),k ; :: thesis: S₁[e, IncAddr (pi p,m),k]
thus S₁[e, IncAddr (pi 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 (pi 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;
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 ;
take IT ; :: thesis: ( dom IT = dom p & ( for m being Element of NAT st m in dom p holds
IT . m = IncAddr (pi 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 (pi p,m),k
let m be Element of NAT ; :: thesis: ( m in dom p implies IT . m = IncAddr (pi p,m),k )
assume m in dom p ; :: thesis: IT . m = IncAddr (pi p,m),k
then ex j being Element of NAT st
( m = j & f . m = IncAddr (pi p,j),k ) by A4;
hence IT . m = IncAddr (pi p,m),k ; :: thesis: verum