defpred S₁[ set , set ] means ex m being Element of NAT st
( $1 = m & $2 = IncAddr ((p /. 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: ( e in dom p implies ex u being set st S₁[e,u] )
assume e in dom p ; :: thesis: ex u being set st S₁[e,u]
then reconsider l = e as Element of NAT by A1;
consider m being natural number such that
A3: l = m ;
take IncAddr ((p /. m),k) ; :: thesis: S₁[e, IncAddr ((p /. m),k)]
thus S₁[e, IncAddr ((p /. m),k)] by A3; :: thesis: verum

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);
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 A7: x in dom f ; :: thesis: f . x in the Object-Kind of S . x
then A8: ex m being Element of NAT st
( x = m & f . x = IncAddr ((p /. m),k) ) by A4, A5;
reconsider y = x as Element of NAT by A1, A4, A7;
the Object-Kind of S . y = the Instructions of S by Def8;
hence f . x in the Object-Kind of S . x by A8; :: thesis: verum

end;

then UU: f is the Object-Kind of S -compatible by FUNCT_1:def 20;
reconsider f = f as finite Element of sproduct the Object-Kind of S by A4, UU, CARD_3:153, FINSET_1:29;
reconsider f = f as FinPartState of S ;
take f ; :: thesis: ( dom f = dom p & ( for m being natural number st m in dom p holds
f . m = IncAddr ((p /. m),k) ) )
thus dom f = dom p by A4; :: thesis: for m being natural number st m in dom p holds
f . m = IncAddr ((p /. m),k)
let m be natural number ; :: thesis: ( m in dom p implies f . m = IncAddr ((p /. m),k) )
assume m in dom p ; :: thesis: f . m = IncAddr ((p /. m),k)
then ex j being Element of NAT st
( m = j & f . m = IncAddr ((p /. j),k) ) by A5;
hence f . m = IncAddr ((p /. m),k) ; :: thesis: verum