set f = the_Values_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:22, ZFMISC_1:31;
A2: dom (the_Values_of SCMPDS) = SCM-Memory by PARTFUN1:def 2;
consider s1 being State of SCMPDS such that
A3: for d being Int_position holds s1 . d = k by Th57;
reconsider S = s1 as SCM-State by CARD_3:107;
set t = S +* (NAT .--> loc);
A4: dom S = the carrier of SCMPDS by PARTFUN1:def 2;
NAT in dom (NAT .--> loc) by TARSKI:def 1;
then A6: (S +* (NAT .--> loc)) . NAT = (NAT .--> loc) . NAT by FUNCT_4:13
.= loc by FUNCOP_1:72 ;
then A7: (S +* (NAT .--> loc)) . NAT in NAT ;
A8: for x being object st x in dom (the_Values_of SCMPDS) holds
(S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x

proof

let x be object ; :: thesis: ( x in dom (the_Values_of SCMPDS) implies (S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x )
assume A9: x in dom (the_Values_of SCMPDS) ; :: thesis: (S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x

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

suppose x = NAT ; :: thesis: (S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x

hence (S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x by A7, AMI_2:6; :: thesis: verum

end;

suppose x <> NAT ; :: thesis: (S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x

then not x in dom (NAT .--> loc) by TARSKI:def 1;
then (S +* (NAT .--> loc)) . x = S . x by FUNCT_4:11;
hence (S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x by A9, CARD_3:9; :: 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}
.= SCM-Memory by A1, XBOOLE_1:12 ;
then reconsider s = S +* (NAT .--> loc) as State of SCMPDS by A2, A8, FUNCT_1:def 14, PARTFUN1:def 2, 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 AMI_2:def 16;
then A10: ex j being Nat st d = [1,j] by AMI_2:23;
not d in dom (NAT .--> loc) by A10, TARSKI:def 1;
hence s . d = s1 . d by FUNCT_4:11
.= k by A3 ;
:: thesis: verum

end;