set f = the Object-Kind of SCMPDS ;
let k be Integer; :: thesis: for loc being Element of NAT ex s being State of SCMPDS st
( s . NAT = loc & ( for d being Int_position holds s . d = k ) )
let loc be Element of NAT ; :: thesis: ex s being State of SCMPDS st
( s . NAT = loc & ( for d being Int_position holds s . d = k ) )
A1: {NAT } c= SCM-Memory by AMI_2:30, ZFMISC_1:37;
A2: dom the Object-Kind of SCMPDS = SCM-Memory by FUNCT_2:def 1;
consider s1 being State of SCMPDS such that
A3: for d being Int_position holds s1 . d = k by Th73;
reconsider S = s1 as SCMPDS-State by PBOOLE:155;
set t = S +* (NAT .--> loc);
A4: dom S = the carrier of SCMPDS by PARTFUN1:def 4;
A5: dom (NAT .--> loc) = {NAT } by FUNCOP_1:19;
then NAT in dom (NAT .--> loc) by TARSKI:def 1;
then A6: (S +* (NAT .--> loc)) . NAT = (NAT .--> loc) . NAT by FUNCT_4:14
.= loc by FUNCOP_1:87 ;
then A7: (S +* (NAT .--> loc)) . NAT in NAT ;
A8: for x being set st x in dom the Object-Kind of SCMPDS holds
(S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x

proof

let x be set ; :: thesis: ( x in dom the Object-Kind of SCMPDS implies (S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x )
assume A9: x in dom the Object-Kind of SCMPDS ; :: thesis: (S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x

per cases ( x = NAT or x <> NAT ) ;

suppose x = NAT ; :: thesis: (S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x

hence (S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x by A7, AMI_2:30, SCMPDS_1:18; :: thesis: verum

end;

suppose x <> NAT ; :: thesis: (S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x

then not x in dom (NAT .--> loc) by A5, TARSKI:def 1;
then (S +* (NAT .--> loc)) . x = S . x by FUNCT_4:12;
hence (S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x by A9, CARD_3:18; :: thesis: verum

end;

end;

end;

dom (S +* (NAT .--> loc)) = (dom S) \/ (dom (NAT .--> loc)) by FUNCT_4:def 1
.= SCM-Memory \/ (dom (NAT .--> loc)) by A4
.= SCM-Memory \/ {NAT } by FUNCOP_1:19
.= SCM-Memory by A1, XBOOLE_1:12 ;
then reconsider s = S +* (NAT .--> loc) as State of SCMPDS by A2, A8, FUNCT_1:def 20, PARTFUN1:def 4, RELAT_1:def 18;
take s ; :: thesis: ( s . NAT = loc & ( for d being Int_position holds s . d = k ) )
thus s . NAT = loc by A6; :: thesis: for d being Int_position holds s . d = k

hereby :: thesis: verum

let d be Int_position ; :: thesis: s . d = k
d in SCM-Data-Loc by Def2;
then A10: ex j being Element of NAT st d = [1,j] by AMI_2:32;

now

assume d in dom (NAT .--> loc) ; :: thesis: contradiction
then d = NAT by A5, TARSKI:def 1;
hence contradiction by A10; :: thesis: verum

end;

hence s . d = s1 . d by FUNCT_4:12
.= k by A3 ;
:: thesis: verum

end;