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);
XX: NAT c= the carrier of S by COMPOS_1:def 2;
dom f c= NAT by A4, RELAT_1:def 18;
then A6: dom f c= the carrier of S by XX, XBOOLE_1:1;
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 COMPOS_1:def 8;
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;
f is the carrier of S -defined Function by A6, RELAT_1:def 18;
then 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