deffunc H₁( Element of NAT ) -> Element of NAT = il. S,($1 + k);
deffunc H₂( Element of NAT ) -> Element of NAT = il. S,$1;
set A = { H₁(m) where m is Element of NAT : H₂(m) in dom p } ;
defpred S₁[ set , set ] means ex m being Element of NAT st
( $1 = il. S,(m + k) & $2 = p . (il. S,m) );
A1: for e being set st e in { H₁(m) where m is Element of NAT : H₂(m) in dom p } holds
ex u being set st S₁[e,u]

proof

let e be set ; :: thesis: ( e in { H₁(m) where m is Element of NAT : H₂(m) in dom p } implies ex u being set st S₁[e,u] )
assume e in { H₁(m) where m is Element of NAT : H₂(m) in dom p } ; :: thesis: ex u being set st S₁[e,u]
then consider m being Element of NAT such that
A2: e = il. S,(m + k) and
il. S,m in dom p ;
take p . (il. S,m) ; :: thesis: S₁[e,p . (il. S,m)]
thus S₁[e,p . (il. S,m)] by A2; :: thesis: verum

end;

consider f being Function such that
A3: dom f = { H₁(m) where m is Element of NAT : H₂(m) in dom p } and
A4: for e being set st e in { H₁(m) where m is Element of NAT : H₂(m) in dom p } holds
S₁[e,f . e] from CLASSES1:sch 1(A1);
A5: NAT c= the carrier of S by AMI_1:def 3;
A6: { H₁(m) where m is Element of NAT : H₂(m) in dom p } c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(m) where m is Element of NAT : H₂(m) in dom p } or x in NAT )
assume x in { H₁(m) where m is Element of NAT : H₂(m) in dom p } ; :: thesis: x in NAT
then ex m being Element of NAT st
( x = il. S,(m + k) & il. S,m in dom p ) ;
hence x in NAT ; :: thesis: verum

end;

then { H₁(m) where m is Element of NAT : H₂(m) in dom p } c= the carrier of S by A5, XBOOLE_1:1;
then A7: dom f c= the carrier of S by A3;
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: ( x in dom f implies f . x in the Object-Kind of S . x )
assume A8: x in dom f ; :: thesis: f . x in the Object-Kind of S . x
then consider m being Element of NAT such that
A9: x = il. S,(m + k) and
A10: f . x = p . (il. S,m) by A3, A4;
reconsider y = x as Element of NAT by A3, A6, A8;
A11: the Object-Kind of S . y = the Instructions of S by AMI_1:def 14;
consider s being State of S such that
A12: p c= s by PBOOLE:156;
consider j being Element of NAT such that
A13: il. S,(m + k) = il. S,(j + k) and
A14: il. S,j in dom p by A3, A8, A9;
A15: j + k = m + k by A13, AMISTD_1:25;
s . (il. S,m) in the Instructions of S ;
hence f . x in the Object-Kind of S . x by A10, A11, A12, A14, A15, GRFUNC_1:8; :: thesis: verum

end;

then X: f is the carrier of S -defined the Object-Kind of S -compatible Function by A7, FUNCT_1:def 20, RELAT_1:def 18;
A16: dom p is finite ;
A17: for m1, m2 being Element of NAT st H₂(m1) = H₂(m2) holds
m1 = m2 by AMISTD_1:25;
{ H₁(m) where m is Element of NAT : H₂(m) in dom p } is finite from FUNCT_7:sch 2(A16, A17);
then reconsider f = f as FinPartState of S by X, A3, FINSET_1:29;
take f ; :: thesis: ( dom f = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } & ( for m being Element of NAT st il. S,m in dom p holds
f . (il. S,(m + k)) = p . (il. S,m) ) )
thus dom f = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } by A3; :: thesis: for m being Element of NAT st il. S,m in dom p holds
f . (il. S,(m + k)) = p . (il. S,m)
let m be Element of NAT ; :: thesis: ( il. S,m in dom p implies f . (il. S,(m + k)) = p . (il. S,m) )
assume il. S,m in dom p ; :: thesis: f . (il. S,(m + k)) = p . (il. S,m)
then il. S,(m + k) in { H₁(m) where m is Element of NAT : H₂(m) in dom p } ;
then consider j being Element of NAT such that
A18: il. S,(m + k) = il. S,(j + k) and
A19: f . (il. S,(m + k)) = p . (il. S,j) by A4;
m + k = j + k by A18, AMISTD_1:25;
hence f . (il. S,(m + k)) = p . (il. S,m) by A19; :: thesis: verum